3. Function Theory🔗

Definition3.1

Group: Functions with an explicit domain, selective union, predicates and relations, and the quantifiers built on them: Hehner's Chapter 3, the prerequisite for the specifications and refinements of Program Theory. The formal counterparts are the Lean modules LaPToP.FunctionTheory.Functions , LaPToP.FunctionTheory.Quantifiers and LaPToP.FunctionTheory.FinePoints . (15)

Group member previews

Preview

Theorem 3.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 4

Reverse dependency previews

Preview

Theorem 3.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

\langle v : D \cdot b \rangle, "map v in D to b", is a function of variable v with domain D (a bunch) and body b; the inclusion v : D is a local axiom within the body. \square f is the domain of f, \# f = {\rm c\llap{/}}\square f its size, and f\,x ("f applied to x") its value at an element x of its domain. x \to y abbreviates \langle v : x \cdot y \rangle with an unused variable.

In Lean a function is a structure Fn α β with a domain dom : Bunch α and a body defined only on the domain, body : (x : α) → x ∈ dom → β; application Fn.apply f x h takes the proof h : x ∈ ☐f, which is the book's local axiom made explicit. Because the body is defined only on the domain, Lean equality of Fn values is exactly Hehner's function equality — same domain, same values on it (Fn.ext). Domains are the bunches of Definition 2.1.

Lean code for Definition3.1●7 declarations

structure(2 fields)defined in LaPToP/FunctionTheory/Functions.lean

complete

structure LaPToP.FunctionTheory.Fn.{u, v} (α : Type u) (β : Type v) :
  Type (max u v)

structure LaPToP.FunctionTheory.Fn.{u, v}
  (α : Type u) (β : Type v) :
  Type (max u v)

A Hehner *function* (aPToP §3.0): a domain (a bunch) together with a body
defined on that domain. `⟨v: D· b⟩` is `Fn.lam D (fun v => b)`.

Fields

dom : LaPToP.BasicTheories.Bunch α

`☐f`, the domain of the function.

body : (x : α) → x ∈ self.dom → β

The body, defined for elements of the domain only.

defdefined in LaPToP/FunctionTheory/Functions.lean

complete

def LaPToP.FunctionTheory.Fn.lam.{u, v} {α : Type u} {β : Type v}
  (D : LaPToP.BasicTheories.Bunch α) (b : α → β) :
  LaPToP.FunctionTheory.Fn α β

def LaPToP.FunctionTheory.Fn.lam.{u, v}
  {α : Type u} {β : Type v}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → β) :
  LaPToP.FunctionTheory.Fn α β

`⟨v: D· b⟩`, the function with domain `D` and body `b`, for a body that does
not need the local axiom `v: D`.

abbrevdefined in LaPToP/FunctionTheory/Functions.lean

complete

abbrev LaPToP.FunctionTheory.Fn.domain.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) : LaPToP.BasicTheories.Bunch α

abbrev LaPToP.FunctionTheory.Fn.domain.{u, v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) :
  LaPToP.BasicTheories.Bunch α

`☐f`, the domain of `f`.

defdefined in LaPToP/FunctionTheory/Functions.lean

complete

def LaPToP.FunctionTheory.Fn.size.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) : ℕ∞

def LaPToP.FunctionTheory.Fn.size.{u, v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) : ℕ∞

`#f = ¢☐f`, the size of a function: the size of its domain.

abbrevdefined in LaPToP/FunctionTheory/Functions.lean

complete

abbrev LaPToP.FunctionTheory.Fn.apply.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) (x : α) (h : x ∈ f.dom) : β

abbrev LaPToP.FunctionTheory.Fn.apply.{u, v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β)
  (x : α) (h : x ∈ f.dom) : β

`f x`, "`f` applied to `x`", for `x` in the domain of `f`.

defdefined in LaPToP/FunctionTheory/Functions.lean

complete

def LaPToP.FunctionTheory.Fn.arrow.{u, v} {α : Type u} {β : Type v} (x : α)
  (y : β) : LaPToP.FunctionTheory.Fn α β

def LaPToP.FunctionTheory.Fn.arrow.{u, v}
  {α : Type u} {β : Type v} (x : α)
  (y : β) : LaPToP.FunctionTheory.Fn α β

`x→y`, "`x` maps to `y`": the function `⟨v: x· y⟩` with an unused variable.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.ext.{u, v} {α : Type u} {β : Type v}
  {f g : LaPToP.FunctionTheory.Fn α β} (hd : f.dom = g.dom)
  (hb :
    ∀ (x : α) (hf : x ∈ f.dom) (hg : x ∈ g.dom),
      f.body x hf = g.body x hg) :
  f = g

theorem LaPToP.FunctionTheory.Fn.ext.{u, v}
  {α : Type u} {β : Type v}
  {f g : LaPToP.FunctionTheory.Fn α β}
  (hd : f.dom = g.dom)
  (hb :
    ∀ (x : α) (hf : x ∈ f.dom)
      (hg : x ∈ g.dom),
      f.body x hf = g.body x hg) :
  f = g

Two functions are equal when they have the same domain and agree on it:
Hehner's function equality.

Theorem3.2

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 2

Reverse dependency previews

Preview

Definition 3.13

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

EffortsmallTagsfunctionhehner-3.0

The axioms of Section 3.0: the Domain Axiom \square\langle v : D \cdot b \rangle = D; \# f = {\rm c\llap{/}}\square f; the Application Axiom x : D \Rightarrow \langle v : D \cdot b \rangle\,x = (\text{substitute } x \text{ for } v \text{ in } b); the Axiom of Extension f = \langle w : \square f \cdot f\,w \rangle; and the Renaming Axiom \langle v : D \cdot b \rangle = \langle w : D \cdot \langle v : D \cdot b \rangle\,w \rangle, which is an instance of Extension. Also (x \to y)\,x = y and \square(x \to y) = x. Uses Definition 3.1.

Lean code for Theorem3.2●7 theorems

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.domain_lam.{u, v} {α : Type u} {β : Type v}
  (D : LaPToP.BasicTheories.Bunch α) (b : α → β) :
  (LaPToP.FunctionTheory.Fn.lam D b).domain = D

theorem LaPToP.FunctionTheory.Fn.domain_lam.{u, v}
  {α : Type u} {β : Type v}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → β) :
  (LaPToP.FunctionTheory.Fn.lam D
        b).domain =
    D

`☐⟨v: D· b⟩ = D` (Domain Axiom).

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.size_eq.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) : f.size = f.domain.size

theorem LaPToP.FunctionTheory.Fn.size_eq.{u, v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) :
  f.size = f.domain.size

`#f = ¢☐f` (size of a function).

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.apply_lam.{u, v} {α : Type u} {β : Type v}
  (D : LaPToP.BasicTheories.Bunch α) (b : α → β) (x : α) (h : x ∈ D) :
  (LaPToP.FunctionTheory.Fn.lam D b).apply x h = b x

theorem LaPToP.FunctionTheory.Fn.apply_lam.{u, v}
  {α : Type u} {β : Type v}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → β) (x : α) (h : x ∈ D) :
  (LaPToP.FunctionTheory.Fn.lam D b).apply
      x h =
    b x

`x: D ⇒ ⟨v: D· b⟩ x = (substitute x for v in b)` (Application Axiom).

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.extension.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) :
  f = { dom := f.domain, body := fun w hw => f.apply w hw }

theorem LaPToP.FunctionTheory.Fn.extension.{u, v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) :
  f =
    { dom := f.domain,
      body := fun w hw => f.apply w hw }

`f = ⟨w: ☐f· f w⟩` (Axiom of Extension).

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.renaming_axiom.{u, v} {α : Type u} {β : Type v}
  (D : LaPToP.BasicTheories.Bunch α) (b : α → β) :
  LaPToP.FunctionTheory.Fn.lam D b =
    { dom := D,
      body := fun w hw =>
        (LaPToP.FunctionTheory.Fn.lam D b).apply w hw }

theorem LaPToP.FunctionTheory.Fn.renaming_axiom.{u,
    v}
  {α : Type u} {β : Type v}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → β) :
  LaPToP.FunctionTheory.Fn.lam D b =
    { dom := D,
      body := fun w hw =>
        (LaPToP.FunctionTheory.Fn.lam D
              b).apply
          w hw }

`⟨v: D· b⟩ = ⟨w: D· ⟨v: D· b⟩ w⟩` (Renaming Axiom), an instance of Extension.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.apply_arrow.{u, v} {α : Type u} {β : Type v}
  (x : α) (y : β) : (LaPToP.FunctionTheory.Fn.arrow x y).apply x ⋯ = y

theorem LaPToP.FunctionTheory.Fn.apply_arrow.{u,
    v}
  {α : Type u} {β : Type v} (x : α)
  (y : β) :
  (LaPToP.FunctionTheory.Fn.arrow x
          y).apply
      x ⋯ =
    y

`(x→y) x = y`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.domain_arrow.{u, v} {α : Type u} {β : Type v}
  (x : α) (y : β) :
  (LaPToP.FunctionTheory.Fn.arrow x y).domain =
    LaPToP.BasicTheories.Bunch.elem x

theorem LaPToP.FunctionTheory.Fn.domain_arrow.{u,
    v}
  {α : Type u} {β : Type v} (x : α)
  (y : β) :
  (LaPToP.FunctionTheory.Fn.arrow x
        y).domain =
    LaPToP.BasicTheories.Bunch.elem x

`☐(x→y) = x`.

Proof for Theorem 3.2

uses 0

All definitional: substitution is β-reduction and Extension is structure eta, so every axiom is rfl.

Definition3.3

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 2.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 3.15

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

f \mid g, "f otherwise g", "behaves like f when applied to an argument in the domain of f, and otherwise behaves like g". Its axioms are \square(f \mid g) = \square f, \square g and (f \mid g)\,x = \mathbf{if}\ x : \square f\ \mathbf{then}\ f\,x\ \mathbf{else}\ g\,x, with the two cases spelled out as corollaries. Uses Definition 3.1 and Theorem 2.3.

Lean code for Definition3.3●5 declarations

defdefined in LaPToP/FunctionTheory/Functions.lean

complete

def LaPToP.FunctionTheory.Fn.orElse.{u, v} {α : Type u} {β : Type v}
  (f g : LaPToP.FunctionTheory.Fn α β) : LaPToP.FunctionTheory.Fn α β

def LaPToP.FunctionTheory.Fn.orElse.{u, v}
  {α : Type u} {β : Type v}
  (f g : LaPToP.FunctionTheory.Fn α β) :
  LaPToP.FunctionTheory.Fn α β

`f | g`, the selective union of `f` and `g`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.domain_orElse.{u, v} {α : Type u} {β : Type v}
  (f g : LaPToP.FunctionTheory.Fn α β) :
  (f.orElse g).domain = f.domain ∪ g.domain

theorem LaPToP.FunctionTheory.Fn.domain_orElse.{u,
    v}
  {α : Type u} {β : Type v}
  (f g : LaPToP.FunctionTheory.Fn α β) :
  (f.orElse g).domain =
    f.domain ∪ g.domain

`☐(f | g) = ☐f, ☐g`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.apply_orElse.{u, v} {α : Type u} {β : Type v}
  (f g : LaPToP.FunctionTheory.Fn α β) (x : α)
  (hx : x ∈ (f.orElse g).domain) :
  (f.orElse g).apply x hx =
    if h : x ∈ f.domain then f.apply x h else g.apply x ⋯

theorem LaPToP.FunctionTheory.Fn.apply_orElse.{u,
    v}
  {α : Type u} {β : Type v}
  (f g : LaPToP.FunctionTheory.Fn α β)
  (x : α) (hx : x ∈ (f.orElse g).domain) :
  (f.orElse g).apply x hx =
    if h : x ∈ f.domain then f.apply x h
    else g.apply x ⋯

`(f | g) x = if x: ☐f then f x else g x`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.apply_orElse_left.{u, v} {α : Type u}
  {β : Type v} (f g : LaPToP.FunctionTheory.Fn α β) (x : α)
  (h : x ∈ f.domain) : (f.orElse g).apply x ⋯ = f.apply x h

theorem LaPToP.FunctionTheory.Fn.apply_orElse_left.{u,
    v}
  {α : Type u} {β : Type v}
  (f g : LaPToP.FunctionTheory.Fn α β)
  (x : α) (h : x ∈ f.domain) :
  (f.orElse g).apply x ⋯ = f.apply x h

`(f | g) x = f x` for `x: ☐f`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.apply_orElse_right.{u, v} {α : Type u}
  {β : Type v} (f g : LaPToP.FunctionTheory.Fn α β) (x : α)
  (h : x ∉ f.domain) (hg : x ∈ g.domain) :
  (f.orElse g).apply x ⋯ = g.apply x hg

theorem LaPToP.FunctionTheory.Fn.apply_orElse_right.{u,
    v}
  {α : Type u} {β : Type v}
  (f g : LaPToP.FunctionTheory.Fn α β)
  (x : α) (h : x ∉ f.domain)
  (hg : x ∈ g.domain) :
  (f.orElse g).apply x ⋯ = g.apply x hg

`(f | g) x = g x` for `x: ☐g` with `¬ x: ☐f`.

Definition3.4

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Definition 3.5

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

"A predicate is a function whose body is a binary expression": Pred α := Fn α Binary, with values in Definition 1.1. The book's examples \mathit{even} = \langle i : \mathit{int} \cdot i/2 : \mathit{int} \rangle and \mathit{odd} = \langle i : \mathit{int} \cdot \neg\, i/2 : \mathit{int} \rangle read "i/2 is an integer" as 2 \mid i. "A relation is a function whose body is a predicate": \mathit{divides} = \langle n : \mathit{nat}+1 \cdot \langle i : \mathit{int} \cdot i/n : \mathit{int} \rangle\rangle, with \mathit{divides}\ 2 = \mathit{even} and \mathit{divides}\ 2\ 3 = \bot checked. Domains are the named bunches of Definition 2.9.

Lean code for Definition3.4●8 declarations

abbrevdefined in LaPToP/FunctionTheory/Functions.lean

complete

abbrev LaPToP.FunctionTheory.Pred.{u} (α : Type u) : Type u

abbrev LaPToP.FunctionTheory.Pred.{u}
  (α : Type u) : Type u

A *predicate*: a function with a binary body.

defdefined in LaPToP/FunctionTheory/Functions.lean

complete

def LaPToP.FunctionTheory.even : LaPToP.FunctionTheory.Pred ℤ

def LaPToP.FunctionTheory.even :
  LaPToP.FunctionTheory.Pred ℤ

`even = ⟨i: int· i/2: int⟩`: `i/2` is an integer, i.e. `2` divides `i`.

defdefined in LaPToP/FunctionTheory/Functions.lean

complete

def LaPToP.FunctionTheory.odd : LaPToP.FunctionTheory.Pred ℤ

def LaPToP.FunctionTheory.odd :
  LaPToP.FunctionTheory.Pred ℤ

`odd = ⟨i: int· ¬ i/2: int⟩`.

defdefined in LaPToP/FunctionTheory/Functions.lean

complete

def LaPToP.FunctionTheory.divides :
  LaPToP.FunctionTheory.Fn ℤ (LaPToP.FunctionTheory.Pred ℤ)

def LaPToP.FunctionTheory.divides :
  LaPToP.FunctionTheory.Fn ℤ
    (LaPToP.FunctionTheory.Pred ℤ)

`divides = ⟨n: nat+1· ⟨i: int· i/n: int⟩⟩`, a relation: a function whose
body is a predicate.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.two_mem_nat_add_one :
  2 ∈ LaPToP.BasicTheories.Bunch.nat + LaPToP.BasicTheories.Bunch.elem 1

theorem LaPToP.FunctionTheory.two_mem_nat_add_one :
  2 ∈
    LaPToP.BasicTheories.Bunch.nat +
      LaPToP.BasicTheories.Bunch.elem 1

`2 : nat+1`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.divides_two :
  LaPToP.FunctionTheory.divides.apply 2
      LaPToP.FunctionTheory.two_mem_nat_add_one =
    LaPToP.FunctionTheory.even

theorem LaPToP.FunctionTheory.divides_two :
  LaPToP.FunctionTheory.divides.apply 2
      LaPToP.FunctionTheory.two_mem_nat_add_one =
    LaPToP.FunctionTheory.even

`divides 2 = even`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.divides_two_three :
  LaPToP.FunctionTheory.Fn.apply
      (LaPToP.FunctionTheory.divides.apply 2
        LaPToP.FunctionTheory.two_mem_nat_add_one)
      3 ⋯ =
    LaPToP.BasicTheories.Binary.bot

theorem LaPToP.FunctionTheory.divides_two_three :
  LaPToP.FunctionTheory.Fn.apply
      (LaPToP.FunctionTheory.divides.apply
        2
        LaPToP.FunctionTheory.two_mem_nat_add_one)
      3 ⋯ =
    LaPToP.BasicTheories.Binary.bot

`divides 2 3 = ⊥`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.odd_apply (i : ℤ)
  (h : i ∈ LaPToP.BasicTheories.Bunch.int) :
  LaPToP.FunctionTheory.Fn.apply LaPToP.FunctionTheory.odd i h =
    !LaPToP.FunctionTheory.Fn.apply LaPToP.FunctionTheory.even i h

theorem LaPToP.FunctionTheory.odd_apply (i : ℤ)
  (h :
    i ∈ LaPToP.BasicTheories.Bunch.int) :
  LaPToP.FunctionTheory.Fn.apply
      LaPToP.FunctionTheory.odd i h =
    !LaPToP.FunctionTheory.Fn.apply
        LaPToP.FunctionTheory.even i h

`odd = ⟨i: int· ¬ even i⟩`: the two examples are complementary.

Definition3.5

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 5

Reverse dependency previews

Preview

Theorem 3.7

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

"A quantifier is a one-operand prefix operator that applies to functions." For a predicate p, \forall p conjoins and \exists p disjoins the results of applying p to all its domain elements. The axioms, for bunches A, B, an element x and a binary body b: \forall v : \mathit{null} \cdot b = \top, \forall v : x \cdot b = \langle v : x \cdot b \rangle\,x, \forall v : A, B \cdot b = (\forall v : A \cdot b) \land (\forall v : B \cdot b), and dually \exists v : \mathit{null} \cdot b = \bot, \exists v : x \cdot b = \langle v : x \cdot b \rangle\,x, \exists v : A, B \cdot b = (\exists v : A \cdot b) \lor (\exists v : B \cdot b). The book's \forall p and \exists p are binary values; over an infinite domain they are not computable, so in Lean they are propositions (Fn.all, Fn.ex) and the axioms are equivalences. Uses Definition 3.4.

Lean code for Definition3.5●8 declarations

defdefined in LaPToP/FunctionTheory/Functions.lean

complete

def LaPToP.FunctionTheory.Fn.all.{u} {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α) : Prop

def LaPToP.FunctionTheory.Fn.all.{u}
  {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α) :
  Prop

`∀p`: `p` holds of every element of its domain.

defdefined in LaPToP/FunctionTheory/Functions.lean

complete

def LaPToP.FunctionTheory.Fn.ex.{u} {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α) : Prop

def LaPToP.FunctionTheory.Fn.ex.{u}
  {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α) :
  Prop

`∃p`: `p` holds of some element of its domain.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_null.{u} {α : Type u}
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam LaPToP.BasicTheories.Bunch.null b).all

theorem LaPToP.FunctionTheory.Fn.all_null.{u}
  {α : Type u}
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam
      LaPToP.BasicTheories.Bunch.null
      b).all

`∀v: null· b = ⊤`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_elem.{u} {α : Type u}
  (b : α → LaPToP.BasicTheories.Binary) (x : α) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.BasicTheories.Bunch.elem x)
        b).all ↔
    b x = true

theorem LaPToP.FunctionTheory.Fn.all_elem.{u}
  {α : Type u}
  (b : α → LaPToP.BasicTheories.Binary)
  (x : α) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.BasicTheories.Bunch.elem
          x)
        b).all ↔
    b x = true

`∀v: x· b = ⟨v: x· b⟩ x`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_union.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B) b).all ↔
    (LaPToP.FunctionTheory.Fn.lam A b).all ∧
      (LaPToP.FunctionTheory.Fn.lam B b).all

theorem LaPToP.FunctionTheory.Fn.all_union.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B)
        b).all ↔
    (LaPToP.FunctionTheory.Fn.lam A
          b).all ∧
      (LaPToP.FunctionTheory.Fn.lam B
          b).all

`∀v: A, B· b = (∀v: A· b) ∧ (∀v: B· b)`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.not_ex_null.{u} {α : Type u}
  (b : α → LaPToP.BasicTheories.Binary) :
  ¬(LaPToP.FunctionTheory.Fn.lam LaPToP.BasicTheories.Bunch.null b).ex

theorem LaPToP.FunctionTheory.Fn.not_ex_null.{u}
  {α : Type u}
  (b : α → LaPToP.BasicTheories.Binary) :
  ¬(LaPToP.FunctionTheory.Fn.lam
        LaPToP.BasicTheories.Bunch.null
        b).ex

`∃v: null· b = ⊥`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_elem.{u} {α : Type u}
  (b : α → LaPToP.BasicTheories.Binary) (x : α) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.BasicTheories.Bunch.elem x)
        b).ex ↔
    b x = true

theorem LaPToP.FunctionTheory.Fn.ex_elem.{u}
  {α : Type u}
  (b : α → LaPToP.BasicTheories.Binary)
  (x : α) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.BasicTheories.Bunch.elem
          x)
        b).ex ↔
    b x = true

`∃v: x· b = ⟨v: x· b⟩ x`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_union.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B) b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam A b).ex ∨
      (LaPToP.FunctionTheory.Fn.lam B b).ex

theorem LaPToP.FunctionTheory.Fn.ex_union.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B)
        b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam A
          b).ex ∨
      (LaPToP.FunctionTheory.Fn.lam B
          b).ex

`∃v: A, B· b = (∃v: A· b) ∨ (∃v: B· b)`.

Definition3.6

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 2.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 6

Reverse dependency previews

Preview

Theorem 3.9

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The solution quantifier \S p, "those", "gives the bunch of solutions of a predicate": \S\langle i : \mathit{int} \cdot i^2 = 4 \rangle = 2, -2. Axioms: \S v : \mathit{null} \cdot b = \mathit{null}, \S v : x \cdot b = \mathbf{if}\ \langle v : x \cdot b \rangle\,x\ \mathbf{then}\ x\ \mathbf{else}\ \mathit{null}, \S v : A, B \cdot b = (\S v : A \cdot b), (\S v : B \cdot b); also \S p : \square p and x : \S p = x : \square p \land p\,x. Uses Definition 3.4 and Definition 2.2.

Lean code for Definition3.6●6 declarations

defdefined in LaPToP/FunctionTheory/Functions.lean

complete

def LaPToP.FunctionTheory.Fn.sols.{u} {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α) : LaPToP.BasicTheories.Bunch α

def LaPToP.FunctionTheory.Fn.sols.{u}
  {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α) :
  LaPToP.BasicTheories.Bunch α

`§p`, the bunch of solutions of `p`: the domain elements of which `p` holds.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.sols_null.{u} {α : Type u}
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam LaPToP.BasicTheories.Bunch.null
        b).sols =
    LaPToP.BasicTheories.Bunch.null

theorem LaPToP.FunctionTheory.Fn.sols_null.{u}
  {α : Type u}
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam
        LaPToP.BasicTheories.Bunch.null
        b).sols =
    LaPToP.BasicTheories.Bunch.null

`§v: null· b = null`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.sols_elem.{u} {α : Type u}
  (b : α → LaPToP.BasicTheories.Binary) (x : α) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.BasicTheories.Bunch.elem x)
        b).sols =
    if b x = true then LaPToP.BasicTheories.Bunch.elem x
    else LaPToP.BasicTheories.Bunch.null

theorem LaPToP.FunctionTheory.Fn.sols_elem.{u}
  {α : Type u}
  (b : α → LaPToP.BasicTheories.Binary)
  (x : α) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.BasicTheories.Bunch.elem
          x)
        b).sols =
    if b x = true then
      LaPToP.BasicTheories.Bunch.elem x
    else LaPToP.BasicTheories.Bunch.null

`§v: x· b = if ⟨v: x· b⟩ x then x else null`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.sols_union.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B) b).sols =
    (LaPToP.FunctionTheory.Fn.lam A b).sols ∪
      (LaPToP.FunctionTheory.Fn.lam B b).sols

theorem LaPToP.FunctionTheory.Fn.sols_union.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B)
        b).sols =
    (LaPToP.FunctionTheory.Fn.lam A
          b).sols ∪
      (LaPToP.FunctionTheory.Fn.lam B
          b).sols

`§v: A, B· b = (§v: A· b), (§v: B· b)`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.sols_subset_domain.{u} {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α) :
  LaPToP.FunctionTheory.Fn.sols p ⊆ LaPToP.FunctionTheory.Fn.domain p

theorem LaPToP.FunctionTheory.Fn.sols_subset_domain.{u}
  {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α) :
  LaPToP.FunctionTheory.Fn.sols p ⊆
    LaPToP.FunctionTheory.Fn.domain p

Solutions lie in the domain: `§p : ☐p`.

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.mem_sols.{u} {α : Type u} (x : α)
  (p : LaPToP.FunctionTheory.Pred α) :
  x ∈ LaPToP.FunctionTheory.Fn.sols p ↔
    ∃ (h : x ∈ LaPToP.FunctionTheory.Fn.domain p),
      LaPToP.FunctionTheory.Fn.apply p x h = true

theorem LaPToP.FunctionTheory.Fn.mem_sols.{u}
  {α : Type u} (x : α)
  (p : LaPToP.FunctionTheory.Pred α) :
  x ∈ LaPToP.FunctionTheory.Fn.sols p ↔
    ∃ (h :
      x ∈
        LaPToP.FunctionTheory.Fn.domain
          p),
      LaPToP.FunctionTheory.Fn.apply p x
          h =
        true

`x: §p = x: ☐p ∧ p x`.

Theorem3.7

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 1.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsfunctionquantifierhehner-3.1

Specialization and Generalization: if p is a predicate and x : \square p, then \forall p \Rightarrow p\,x \Rightarrow \exists p. The One-Point Laws: if x : D (and v does not appear in x), \forall v : D \cdot v = x \Rightarrow b \;=\; \langle v : D \cdot b \rangle\,x and \exists v : D \cdot v = x \land b \;=\; \langle v : D \cdot b \rangle\,x. Uses Definition 3.5 and Theorem 1.3.

Lean code for Theorem3.7●5 theorems

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_apply.{u} {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α) (x : α)
  (hp : LaPToP.FunctionTheory.Fn.all p)
  (h : x ∈ LaPToP.FunctionTheory.Fn.domain p) :
  LaPToP.FunctionTheory.Fn.apply p x h = true

theorem LaPToP.FunctionTheory.Fn.all_apply.{u}
  {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α)
  (x : α)
  (hp : LaPToP.FunctionTheory.Fn.all p)
  (h :
    x ∈
      LaPToP.FunctionTheory.Fn.domain p) :
  LaPToP.FunctionTheory.Fn.apply p x h =
    true

`∀p ⇒ p x` for `x: ☐p` (Specialization).

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_of_apply.{u} {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α) (x : α)
  (h : x ∈ LaPToP.FunctionTheory.Fn.domain p)
  (hx : LaPToP.FunctionTheory.Fn.apply p x h = true) :
  LaPToP.FunctionTheory.Fn.ex p

theorem LaPToP.FunctionTheory.Fn.ex_of_apply.{u}
  {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α)
  (x : α)
  (h :
    x ∈ LaPToP.FunctionTheory.Fn.domain p)
  (hx :
    LaPToP.FunctionTheory.Fn.apply p x h =
      true) :
  LaPToP.FunctionTheory.Fn.ex p

`p x ⇒ ∃p` for `x: ☐p` (Generalization).

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_of_all.{u} {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α) (x : α)
  (hp : LaPToP.FunctionTheory.Fn.all p)
  (h : x ∈ LaPToP.FunctionTheory.Fn.domain p) :
  LaPToP.FunctionTheory.Fn.ex p

theorem LaPToP.FunctionTheory.Fn.ex_of_all.{u}
  {α : Type u}
  (p : LaPToP.FunctionTheory.Pred α)
  (x : α)
  (hp : LaPToP.FunctionTheory.Fn.all p)
  (h :
    x ∈
      LaPToP.FunctionTheory.Fn.domain p) :
  LaPToP.FunctionTheory.Fn.ex p

`∀p ⇒ ∃p` when the domain is nonempty (Specialization then Generalization).

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_eq_imp.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) (x : α) [DecidableEq α]
  (hx : x ∈ D) :
  (LaPToP.FunctionTheory.Fn.lam D fun v =>
        LaPToP.BasicTheories.Binary.imp (decide (v = x)) (b v)).all ↔
    b x = true

theorem LaPToP.FunctionTheory.Fn.all_eq_imp.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary)
  (x : α) [DecidableEq α] (hx : x ∈ D) :
  (LaPToP.FunctionTheory.Fn.lam D fun v =>
        LaPToP.BasicTheories.Binary.imp
          (decide (v = x)) (b v)).all ↔
    b x = true

`∀v: D· v=x ⇒ b = ⟨v: D· b⟩ x` for `x: D` (One-Point Law).

theoremdefined in LaPToP/FunctionTheory/Functions.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_eq_and.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) (x : α) [DecidableEq α]
  (hx : x ∈ D) :
  (LaPToP.FunctionTheory.Fn.lam D fun v => decide (v = x) && b v).ex ↔
    b x = true

theorem LaPToP.FunctionTheory.Fn.ex_eq_and.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary)
  (x : α) [DecidableEq α] (hx : x ∈ D) :
  (LaPToP.FunctionTheory.Fn.lam D fun v =>
        decide (v = x) && b v).ex ↔
    b x = true

`∃v: D· v=x ∧ b = ⟨v: D· b⟩ x` for `x: D` (One-Point Law).

Proof for Theorem 3.7

uses 0

Specialization instantiates the universal at x; Generalization exhibits x. For One-Point, the antecedent/conjunct v = x pins the variable, and the equality is decided in Bool.

Definition3.8

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 2.17

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 6

Reverse dependency previews

Preview

Theorem 3.9

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

"Any two-operand symmetric associative operator can be used to define a quantifier": +, \times, \uparrow, \downarrow give \Sigma, \Pi, \Uparrow, \Downarrow. For a numeric function f, \Uparrow f and \Downarrow f are the least upper bound and greatest lower bound of the results of f on its domain (its range, Fn.values), taken in the extended reals of Definition 2.17, which form a complete linear order; \uparrow/\downarrow are \sqcup/\sqcap (\max/\min). \Sigma f and \Pi f are Mathlib's finite sum and product over the domain. These are faithful only for finite domains — Mathlib's ∑ᶠ is 0 when the support is infinite, whereas the book's \Sigma n : \mathit{nat}+1 \cdot 1/2^n = 1 is a convergent series; the laws below that split a domain carry finiteness hypotheses, and nothing here claims anything about infinite sums. Uses Definition 3.1.

Lean code for Definition3.8●7 declarations

defdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

def LaPToP.FunctionTheory.Fn.values.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) : LaPToP.BasicTheories.Bunch β

def LaPToP.FunctionTheory.Fn.values.{u, v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) :
  LaPToP.BasicTheories.Bunch β

The *range* of a function (aPToP §3.0): the elements obtained by applying
it to each element of its domain.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.values_lam.{u, v} {α : Type u} {β : Type v}
  (D : LaPToP.BasicTheories.Bunch α) (b : α → β) :
  (LaPToP.FunctionTheory.Fn.lam D b).values = b '' D

theorem LaPToP.FunctionTheory.Fn.values_lam.{u, v}
  {α : Type u} {β : Type v}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → β) :
  (LaPToP.FunctionTheory.Fn.lam D
        b).values =
    b '' D

The range of `⟨v: D· b⟩` is the image of `D` under `b`.

defdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

def LaPToP.FunctionTheory.Fn.sup.{u} {α : Type u}
  (f : LaPToP.FunctionTheory.Fn α LaPToP.BasicTheories.Number) :
  LaPToP.BasicTheories.Number

def LaPToP.FunctionTheory.Fn.sup.{u}
  {α : Type u}
  (f :
    LaPToP.FunctionTheory.Fn α
      LaPToP.BasicTheories.Number) :
  LaPToP.BasicTheories.Number

`⇑f`, the maximum (least upper bound) of the results of `f`.

defdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

def LaPToP.FunctionTheory.Fn.inf.{u} {α : Type u}
  (f : LaPToP.FunctionTheory.Fn α LaPToP.BasicTheories.Number) :
  LaPToP.BasicTheories.Number

def LaPToP.FunctionTheory.Fn.inf.{u}
  {α : Type u}
  (f :
    LaPToP.FunctionTheory.Fn α
      LaPToP.BasicTheories.Number) :
  LaPToP.BasicTheories.Number

`⇓f`, the minimum (greatest lower bound) of the results of `f`.

defdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

def LaPToP.FunctionTheory.Fn.sum.{u} {α : Type u}
  (f : LaPToP.FunctionTheory.Fn α LaPToP.BasicTheories.Number) :
  LaPToP.BasicTheories.Number

def LaPToP.FunctionTheory.Fn.sum.{u}
  {α : Type u}
  (f :
    LaPToP.FunctionTheory.Fn α
      LaPToP.BasicTheories.Number) :
  LaPToP.BasicTheories.Number

`Σf`, the sum of the results of `f` — for a finite domain (see the module
docstring).

defdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

def LaPToP.FunctionTheory.Fn.prod.{u} {α : Type u}
  (f : LaPToP.FunctionTheory.Fn α LaPToP.BasicTheories.Number) :
  LaPToP.BasicTheories.Number

def LaPToP.FunctionTheory.Fn.prod.{u}
  {α : Type u}
  (f :
    LaPToP.FunctionTheory.Fn α
      LaPToP.BasicTheories.Number) :
  LaPToP.BasicTheories.Number

`Πf`, the product of the results of `f` — for a finite domain (see the
module docstring).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sup_eq_max
  (a b : LaPToP.BasicTheories.Number) : max a b = max a b

theorem LaPToP.FunctionTheory.Fn.sup_eq_max
  (a b : LaPToP.BasicTheories.Number) :
  max a b = max a b

`↑` and `↓` are `max` and `min`.

Theorem3.9

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Theorem 2.6

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsfunctionquantifierhehner-3.1

The axioms of Section 3.1 for the numeric quantifiers, for bunches A, B, D, an element x, a number body n and a binary b: \Sigma v : \mathit{null} \cdot n = 0, \Sigma v : x \cdot n = \langle v : x \cdot n \rangle\,x, (\Sigma v : A, B \cdot n) + (\Sigma v : A \mathbin{\lq} B \cdot n) = (\Sigma v : A \cdot n) + (\Sigma v : B \cdot n); \Pi likewise with 1 and \times; \Downarrow v : \mathit{null} \cdot n = \infty, \Downarrow v : x \cdot n = \langle v : x \cdot n \rangle\,x, \Downarrow v : A, B \cdot n = (\Downarrow v : A \cdot n) \downarrow (\Downarrow v : B \cdot n); \Uparrow likewise with -\infty and \uparrow; and the \S-domain laws \Sigma v : (\S v : D \cdot b) \cdot n = \Sigma v : D \cdot \mathbf{if}\ b\ \mathbf{then}\ n\ \mathbf{else}\ 0 (and 1, \infty, -\infty for \Pi, \Downarrow, \Uparrow). Also Cardinality {\rm c\llap{/}}A = \Sigma(A \to 1) for finite A. The \Sigma/\Pi splitting laws are stated for finite A, B. Uses Definition 3.8, Definition 3.6 and Theorem 2.6.

Lean code for Theorem3.9●17 theorems

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sup_null.{u} {α : Type u}
  (n : α → LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam LaPToP.BasicTheories.Bunch.null n).sup =
    ⊥

theorem LaPToP.FunctionTheory.Fn.sup_null.{u}
  {α : Type u}
  (n : α → LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam
        LaPToP.BasicTheories.Bunch.null
        n).sup =
    ⊥

`⇑v: null· n = –∞`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.inf_null.{u} {α : Type u}
  (n : α → LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam LaPToP.BasicTheories.Bunch.null n).inf =
    ⊤

theorem LaPToP.FunctionTheory.Fn.inf_null.{u}
  {α : Type u}
  (n : α → LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam
        LaPToP.BasicTheories.Bunch.null
        n).inf =
    ⊤

`⇓v: null· n = ∞`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sup_elem.{u} {α : Type u}
  (n : α → LaPToP.BasicTheories.Number) (x : α) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.BasicTheories.Bunch.elem x)
        n).sup =
    n x

theorem LaPToP.FunctionTheory.Fn.sup_elem.{u}
  {α : Type u}
  (n : α → LaPToP.BasicTheories.Number)
  (x : α) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.BasicTheories.Bunch.elem
          x)
        n).sup =
    n x

`⇑v: x· n = ⟨v: x· n⟩ x`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.inf_elem.{u} {α : Type u}
  (n : α → LaPToP.BasicTheories.Number) (x : α) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.BasicTheories.Bunch.elem x)
        n).inf =
    n x

theorem LaPToP.FunctionTheory.Fn.inf_elem.{u}
  {α : Type u}
  (n : α → LaPToP.BasicTheories.Number)
  (x : α) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.BasicTheories.Bunch.elem
          x)
        n).inf =
    n x

`⇓v: x· n = ⟨v: x· n⟩ x`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sup_union.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B) n).sup =
    max (LaPToP.FunctionTheory.Fn.lam A n).sup
      (LaPToP.FunctionTheory.Fn.lam B n).sup

theorem LaPToP.FunctionTheory.Fn.sup_union.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B)
        n).sup =
    max
      (LaPToP.FunctionTheory.Fn.lam A
          n).sup
      (LaPToP.FunctionTheory.Fn.lam B
          n).sup

`⇑v: A, B· n = (⇑v: A· n) ↑ (⇑v: B· n)`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.inf_union.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B) n).inf =
    min (LaPToP.FunctionTheory.Fn.lam A n).inf
      (LaPToP.FunctionTheory.Fn.lam B n).inf

theorem LaPToP.FunctionTheory.Fn.inf_union.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B)
        n).inf =
    min
      (LaPToP.FunctionTheory.Fn.lam A
          n).inf
      (LaPToP.FunctionTheory.Fn.lam B
          n).inf

`⇓v: A, B· n = (⇓v: A· n) ↓ (⇓v: B· n)`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sup_sols.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.FunctionTheory.Fn.lam D b).sols
        n).sup =
    (LaPToP.FunctionTheory.Fn.lam D fun v =>
        if b v = true then n v else ⊥).sup

theorem LaPToP.FunctionTheory.Fn.sup_sols.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.FunctionTheory.Fn.lam D
            b).sols
        n).sup =
    (LaPToP.FunctionTheory.Fn.lam D
        fun v =>
        if b v = true then n v else ⊥).sup

`⇑v: (§v: D· b)· n = ⇑v: D· if b then n else –∞`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.inf_sols.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.FunctionTheory.Fn.lam D b).sols
        n).inf =
    (LaPToP.FunctionTheory.Fn.lam D fun v =>
        if b v = true then n v else ⊤).inf

theorem LaPToP.FunctionTheory.Fn.inf_sols.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.FunctionTheory.Fn.lam D
            b).sols
        n).inf =
    (LaPToP.FunctionTheory.Fn.lam D
        fun v =>
        if b v = true then n v else ⊤).inf

`⇓v: (§v: D· b)· n = ⇓v: D· if b then n else ∞`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sum_null.{u} {α : Type u}
  (n : α → LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam LaPToP.BasicTheories.Bunch.null n).sum =
    0

theorem LaPToP.FunctionTheory.Fn.sum_null.{u}
  {α : Type u}
  (n : α → LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam
        LaPToP.BasicTheories.Bunch.null
        n).sum =
    0

`Σv: null· n = 0`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sum_elem.{u} {α : Type u}
  (n : α → LaPToP.BasicTheories.Number) (x : α) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.BasicTheories.Bunch.elem x)
        n).sum =
    n x

theorem LaPToP.FunctionTheory.Fn.sum_elem.{u}
  {α : Type u}
  (n : α → LaPToP.BasicTheories.Number)
  (x : α) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.BasicTheories.Bunch.elem
          x)
        n).sum =
    n x

`Σv: x· n = ⟨v: x· n⟩ x`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sum_union_add_sum_inter.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number) (hA : Set.Finite A)
  (hB : Set.Finite B) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B) n).sum +
      (LaPToP.FunctionTheory.Fn.lam (A ∩ B) n).sum =
    (LaPToP.FunctionTheory.Fn.lam A n).sum +
      (LaPToP.FunctionTheory.Fn.lam B n).sum

theorem LaPToP.FunctionTheory.Fn.sum_union_add_sum_inter.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number)
  (hA : Set.Finite A)
  (hB : Set.Finite B) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B)
          n).sum +
      (LaPToP.FunctionTheory.Fn.lam
          (A ∩ B) n).sum =
    (LaPToP.FunctionTheory.Fn.lam A
          n).sum +
      (LaPToP.FunctionTheory.Fn.lam B
          n).sum

`(Σv: A, B· n) + (Σv: A‘B· n) = (Σv: A· n) + (Σv: B· n)`, for finite `A`, `B`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sum_sols.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.FunctionTheory.Fn.lam D b).sols
        n).sum =
    (LaPToP.FunctionTheory.Fn.lam D fun v =>
        if b v = true then n v else 0).sum

theorem LaPToP.FunctionTheory.Fn.sum_sols.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.FunctionTheory.Fn.lam D
            b).sols
        n).sum =
    (LaPToP.FunctionTheory.Fn.lam D
        fun v =>
        if b v = true then n v else 0).sum

`Σv: (§v: D· b)· n = Σv: D· if b then n else 0`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.prod_null.{u} {α : Type u}
  (n : α → LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam LaPToP.BasicTheories.Bunch.null
        n).prod =
    1

theorem LaPToP.FunctionTheory.Fn.prod_null.{u}
  {α : Type u}
  (n : α → LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam
        LaPToP.BasicTheories.Bunch.null
        n).prod =
    1

`Πv: null· n = 1`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.prod_elem.{u} {α : Type u}
  (n : α → LaPToP.BasicTheories.Number) (x : α) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.BasicTheories.Bunch.elem x)
        n).prod =
    n x

theorem LaPToP.FunctionTheory.Fn.prod_elem.{u}
  {α : Type u}
  (n : α → LaPToP.BasicTheories.Number)
  (x : α) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.BasicTheories.Bunch.elem
          x)
        n).prod =
    n x

`Πv: x· n = ⟨v: x· n⟩ x`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.prod_union_mul_prod_inter.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number) (hA : Set.Finite A)
  (hB : Set.Finite B) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B) n).prod *
      (LaPToP.FunctionTheory.Fn.lam (A ∩ B) n).prod =
    (LaPToP.FunctionTheory.Fn.lam A n).prod *
      (LaPToP.FunctionTheory.Fn.lam B n).prod

theorem LaPToP.FunctionTheory.Fn.prod_union_mul_prod_inter.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number)
  (hA : Set.Finite A)
  (hB : Set.Finite B) :
  (LaPToP.FunctionTheory.Fn.lam (A ∪ B)
          n).prod *
      (LaPToP.FunctionTheory.Fn.lam
          (A ∩ B) n).prod =
    (LaPToP.FunctionTheory.Fn.lam A
          n).prod *
      (LaPToP.FunctionTheory.Fn.lam B
          n).prod

`(Πv: A, B· n) × (Πv: A‘B· n) = (Πv: A· n) × (Πv: B· n)`, for finite `A`, `B`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.prod_sols.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.FunctionTheory.Fn.lam D b).sols
        n).prod =
    (LaPToP.FunctionTheory.Fn.lam D fun v =>
        if b v = true then n v else 1).prod

theorem LaPToP.FunctionTheory.Fn.prod_sols.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (n : α → LaPToP.BasicTheories.Number)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.FunctionTheory.Fn.lam D
            b).sols
        n).prod =
    (LaPToP.FunctionTheory.Fn.lam D
        fun v =>
        if b v = true then n v
        else 1).prod

`Πv: (§v: D· b)· n = Πv: D· if b then n else 1`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.size_eq_sum_one.{u} {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) (hA : Set.Finite A) :
  ∃ k,
    A.size = ↑k ∧ (LaPToP.FunctionTheory.Fn.lam A fun x => 1).sum = ↑k

theorem LaPToP.FunctionTheory.Fn.size_eq_sum_one.{u}
  {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α)
  (hA : Set.Finite A) :
  ∃ k,
    A.size = ↑k ∧
      (LaPToP.FunctionTheory.Fn.lam A
            fun x => 1).sum =
        ↑k

`¢A = Σ(A→1)` (Cardinality), for finite `A`: both sides are the number of
elements of `A`.

Proof for Theorem 3.9

uses 0

\Uparrow/\Downarrow: sSup/sInf of the empty set, a singleton, a union (sSup_union); the \S-domain law by antisymmetry of \le. \Sigma/\Pi: finsum_mem_empty, finsum_mem_singleton, finsum_mem_union_inter, and restriction to the support for the \S-domain law.

Theorem3.10

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 2.20

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsfunctionquantifierhehner-11.3.8

Laws of §11.3.8 for \Uparrow, \Downarrow: Specialize and Generalize \Downarrow f \le f\,x \le \Uparrow f for x : \square f; Duality -\Uparrow v \cdot n = \Downarrow v \cdot -n, -\Downarrow v \cdot n = \Uparrow v \cdot -n; Bounding n \ge (\Uparrow v : D \cdot m) = (\forall v : D \cdot n \ge m), n \le (\Downarrow v : D \cdot m) = (\forall v : D \cdot n \le m), n > (\Downarrow v : D \cdot m) = (\exists v : D \cdot n > m), n < (\Uparrow v : D \cdot m) = (\exists v : D \cdot n < m), and the four one-directional forms (the book's proviso D \neq \mathit{null} is not needed for these); Extreme (\Downarrow n : \mathit{int} \cdot n) = -\infty, (\Uparrow n : \mathit{int} \cdot n) = \infty; Connection n \le m = \forall k \cdot k \le n \Rightarrow k \le m and its three variants; Change of Variable \Uparrow r : f\,D \cdot b = \Uparrow d : D \cdot \langle r : f\,D \cdot b \rangle (f\,d) and dually. The distributive laws of + - \times \uparrow \downarrow over \Uparrow \Downarrow are deferred. Uses Definition 3.8 and Theorem 2.20.

Lean code for Theorem3.10●21 theorems

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.inf_le_apply.{u} {α : Type u}
  (f : LaPToP.FunctionTheory.Fn α LaPToP.BasicTheories.Number) (x : α)
  (h : x ∈ f.domain) : f.inf ≤ f.apply x h

theorem LaPToP.FunctionTheory.Fn.inf_le_apply.{u}
  {α : Type u}
  (f :
    LaPToP.FunctionTheory.Fn α
      LaPToP.BasicTheories.Number)
  (x : α) (h : x ∈ f.domain) :
  f.inf ≤ f.apply x h

`⇓f ≤ f x` for `x: ☐f` (Specialize).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.apply_le_sup.{u} {α : Type u}
  (f : LaPToP.FunctionTheory.Fn α LaPToP.BasicTheories.Number) (x : α)
  (h : x ∈ f.domain) : f.apply x h ≤ f.sup

theorem LaPToP.FunctionTheory.Fn.apply_le_sup.{u}
  {α : Type u}
  (f :
    LaPToP.FunctionTheory.Fn α
      LaPToP.BasicTheories.Number)
  (x : α) (h : x ∈ f.domain) :
  f.apply x h ≤ f.sup

`f x ≤ ⇑f` for `x: ☐f` (Generalize).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.neg_sSup
  (S : Set LaPToP.BasicTheories.Number) :
  -sSup S = sInf ((fun y => -y) '' S)

theorem LaPToP.FunctionTheory.Fn.neg_sSup
  (S : Set LaPToP.BasicTheories.Number) :
  -sSup S = sInf ((fun y => -y) '' S)

`–sSup S = sInf (–S)` in the extended reals.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.neg_sup.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number) :
  -(LaPToP.FunctionTheory.Fn.lam D m).sup =
    (LaPToP.FunctionTheory.Fn.lam D fun v => -m v).inf

theorem LaPToP.FunctionTheory.Fn.neg_sup.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number) :
  -(LaPToP.FunctionTheory.Fn.lam D
          m).sup =
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => -m v).inf

`–⇑v· n = ⇓v· –n` (Duality).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.neg_inf.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number) :
  -(LaPToP.FunctionTheory.Fn.lam D m).inf =
    (LaPToP.FunctionTheory.Fn.lam D fun v => -m v).sup

theorem LaPToP.FunctionTheory.Fn.neg_inf.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number) :
  -(LaPToP.FunctionTheory.Fn.lam D
          m).inf =
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => -m v).sup

`–⇓v· n = ⇑v· –n` (Duality).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sup_le_iff.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam D m).sup ≤ n ↔ ∀ v ∈ D, m v ≤ n

theorem LaPToP.FunctionTheory.Fn.sup_le_iff.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam D m).sup ≤
      n ↔
    ∀ v ∈ D, m v ≤ n

`n ≥ (⇑v: D· m) = (∀v: D· n ≥ m)` (Bounding).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.le_inf_iff.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number) :
  n ≤ (LaPToP.FunctionTheory.Fn.lam D m).inf ↔ ∀ v ∈ D, n ≤ m v

theorem LaPToP.FunctionTheory.Fn.le_inf_iff.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number) :
  n ≤
      (LaPToP.FunctionTheory.Fn.lam D
          m).inf ↔
    ∀ v ∈ D, n ≤ m v

`n ≤ (⇓v: D· m) = (∀v: D· n ≤ m)` (Bounding).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.inf_lt_iff.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam D m).inf < n ↔ ∃ v ∈ D, m v < n

theorem LaPToP.FunctionTheory.Fn.inf_lt_iff.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number) :
  (LaPToP.FunctionTheory.Fn.lam D m).inf <
      n ↔
    ∃ v ∈ D, m v < n

`n > (⇓v: D· m) = (∃v: D· n > m)` (Bounding).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.lt_sup_iff.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number) :
  n < (LaPToP.FunctionTheory.Fn.lam D m).sup ↔ ∃ v ∈ D, n < m v

theorem LaPToP.FunctionTheory.Fn.lt_sup_iff.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number) :
  n <
      (LaPToP.FunctionTheory.Fn.lam D
          m).sup ↔
    ∃ v ∈ D, n < m v

`n < (⇑v: D· m) = (∃v: D· n < m)` (Bounding).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.forall_lt_of_sup_lt.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number)
  (h : (LaPToP.FunctionTheory.Fn.lam D m).sup < n) (v : α) :
  v ∈ D → m v < n

theorem LaPToP.FunctionTheory.Fn.forall_lt_of_sup_lt.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number)
  (h :
    (LaPToP.FunctionTheory.Fn.lam D
          m).sup <
      n)
  (v : α) : v ∈ D → m v < n

`n > (⇑v: D· m) ⇒ (∀v: D· n > m)` (Bounding).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.forall_lt_of_lt_inf.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number)
  (h : n < (LaPToP.FunctionTheory.Fn.lam D m).inf) (v : α) :
  v ∈ D → n < m v

theorem LaPToP.FunctionTheory.Fn.forall_lt_of_lt_inf.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number)
  (h :
    n <
      (LaPToP.FunctionTheory.Fn.lam D
          m).inf)
  (v : α) : v ∈ D → n < m v

`n < (⇓v: D· m) ⇒ (∀v: D· n < m)` (Bounding).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.inf_le_of_exists.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number) (h : ∃ v ∈ D, m v ≤ n) :
  (LaPToP.FunctionTheory.Fn.lam D m).inf ≤ n

theorem LaPToP.FunctionTheory.Fn.inf_le_of_exists.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number)
  (h : ∃ v ∈ D, m v ≤ n) :
  (LaPToP.FunctionTheory.Fn.lam D m).inf ≤
    n

`n ≥ (⇓v: D· m) ⇐ (∃v: D· n ≥ m)` (Bounding).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.le_sup_of_exists.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number) (h : ∃ v ∈ D, n ≤ m v) :
  n ≤ (LaPToP.FunctionTheory.Fn.lam D m).sup

theorem LaPToP.FunctionTheory.Fn.le_sup_of_exists.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (m : α → LaPToP.BasicTheories.Number)
  (n : LaPToP.BasicTheories.Number)
  (h : ∃ v ∈ D, n ≤ m v) :
  n ≤
    (LaPToP.FunctionTheory.Fn.lam D m).sup

`n ≤ (⇑v: D· m) ⇐ (∃v: D· n ≤ m)` (Bounding).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.inf_int :
  (LaPToP.FunctionTheory.Fn.lam LaPToP.BasicTheories.Bunch.int fun k =>
        ↑↑k).inf =
    ⊥

theorem LaPToP.FunctionTheory.Fn.inf_int :
  (LaPToP.FunctionTheory.Fn.lam
        LaPToP.BasicTheories.Bunch.int
        fun k => ↑↑k).inf =
    ⊥

`(⇓n: int· n) = –∞` (Extreme): the integers are unbounded below.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sup_int :
  (LaPToP.FunctionTheory.Fn.lam LaPToP.BasicTheories.Bunch.int fun k =>
        ↑↑k).sup =
    ⊤

theorem LaPToP.FunctionTheory.Fn.sup_int :
  (LaPToP.FunctionTheory.Fn.lam
        LaPToP.BasicTheories.Bunch.int
        fun k => ↑↑k).sup =
    ⊤

`(⇑n: int· n) = ∞` (Extreme): the integers are unbounded above.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.le_iff_forall_le_imp
  (n m : LaPToP.BasicTheories.Number) : n ≤ m ↔ ∀ k ≤ n, k ≤ m

theorem LaPToP.FunctionTheory.Fn.le_iff_forall_le_imp
  (n m : LaPToP.BasicTheories.Number) :
  n ≤ m ↔ ∀ k ≤ n, k ≤ m

`n ≤ m = ∀k· k ≤ n ⇒ k ≤ m` (Connection).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.le_iff_forall_lt_imp
  (n m : LaPToP.BasicTheories.Number) : n ≤ m ↔ ∀ k < n, k < m

theorem LaPToP.FunctionTheory.Fn.le_iff_forall_lt_imp
  (n m : LaPToP.BasicTheories.Number) :
  n ≤ m ↔ ∀ k < n, k < m

`n ≤ m = ∀k· k < n ⇒ k < m` (Connection).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.le_iff_forall_le_imp'
  (n m : LaPToP.BasicTheories.Number) :
  n ≤ m ↔ ∀ (k : LaPToP.BasicTheories.Number), m ≤ k → n ≤ k

theorem LaPToP.FunctionTheory.Fn.le_iff_forall_le_imp'
  (n m : LaPToP.BasicTheories.Number) :
  n ≤ m ↔
    ∀ (k : LaPToP.BasicTheories.Number),
      m ≤ k → n ≤ k

`n ≤ m = ∀k· m ≤ k ⇒ n ≤ k` (Connection).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.le_iff_forall_lt_imp'
  (n m : LaPToP.BasicTheories.Number) :
  n ≤ m ↔ ∀ (k : LaPToP.BasicTheories.Number), m < k → n < k

theorem LaPToP.FunctionTheory.Fn.le_iff_forall_lt_imp'
  (n m : LaPToP.BasicTheories.Number) :
  n ≤ m ↔
    ∀ (k : LaPToP.BasicTheories.Number),
      m < k → n < k

`n ≤ m = ∀k· m < k ⇒ n < k` (Connection).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sup_image.{u, v} {α : Type u} {β : Type v}
  (m : α → LaPToP.BasicTheories.Number) (g : β → α)
  (E : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.lam (g '' E) m).sup =
    (LaPToP.FunctionTheory.Fn.lam E fun d => m (g d)).sup

theorem LaPToP.FunctionTheory.Fn.sup_image.{u, v}
  {α : Type u} {β : Type v}
  (m : α → LaPToP.BasicTheories.Number)
  (g : β → α)
  (E : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.lam (g '' E)
        m).sup =
    (LaPToP.FunctionTheory.Fn.lam E
        fun d => m (g d)).sup

`⇑r: f D· b = ⇑d: D· ⟨r: f D· b⟩ (f d)` (Change of Variable).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.inf_image.{u, v} {α : Type u} {β : Type v}
  (m : α → LaPToP.BasicTheories.Number) (g : β → α)
  (E : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.lam (g '' E) m).inf =
    (LaPToP.FunctionTheory.Fn.lam E fun d => m (g d)).inf

theorem LaPToP.FunctionTheory.Fn.inf_image.{u, v}
  {α : Type u} {β : Type v}
  (m : α → LaPToP.BasicTheories.Number)
  (g : β → α)
  (E : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.lam (g '' E)
        m).inf =
    (LaPToP.FunctionTheory.Fn.lam E
        fun d => m (g d)).inf

`⇓r: f D· b = ⇓d: D· ⟨r: f D· b⟩ (f d)` (Change of Variable).

Proof for Theorem 3.10

uses 0

le_sSup/sInf_le, sSup_le_iff/le_sInf_iff, lt_sSup_iff/sInf_lt_iff; Duality by antisymmetry using a \le -b = b \le -a; Extreme by sInf_eq_bot/ sSup_eq_top with \lfloor r \rfloor - 1 and \lceil r \rceil + 1 as witnesses.

Theorem3.11

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 1.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsfunctionquantifierhehner-11.3.8

Laws of §11.3.8 for \forall, \exists: Identity \forall v \cdot \top, \neg\exists v \cdot \bot; Idempotent \forall v : D \cdot b = b, \exists v : D \cdot b = b for D \neq \mathit{null} and v not in b; Duality \neg\forall v \cdot b = \exists v \cdot \neg b, \neg\exists v \cdot b = \forall v \cdot \neg b; Distributive a \land \forall v : D \cdot b = \forall v : D \cdot a \land b and the five companions with \land \lor \Rightarrow over \forall \exists; Antidistributive a \Leftarrow \exists v : D \cdot b = \forall v : D \cdot a \Leftarrow b, a \Leftarrow \forall v : D \cdot b = \exists v : D \cdot a \Leftarrow b (the book's proviso D \neq \mathit{null} is carried exactly where it is needed); Absorption (four laws, for x : D); Splitting (eight laws, e.g. \forall v \cdot a \land b = (\forall v \cdot a) \land (\forall v \cdot b), \exists v \cdot a \land b \Rightarrow (\exists v \cdot a) \land (\exists v \cdot b)); Commutative \forall v \cdot \forall w \cdot b = \forall w \cdot \forall v \cdot b and for \exists; Semicommutative \exists v \cdot \forall w \cdot b \Rightarrow \forall w \cdot \exists v \cdot b and \forall x \cdot \exists y \cdot p\,x\,y = \exists f \cdot \forall x \cdot p\,x\,(f\,x); Change of Variable. Since \forall p is a proposition here, nested quantifications are written as iterated bounded quantifiers. Uses Definition 3.5 and Theorem 1.4.

Lean code for Theorem3.11●34 theorems

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_lam.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D b).all ↔ ∀ x ∈ D, b x = true

theorem LaPToP.FunctionTheory.Fn.all_lam.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D b).all ↔
    ∀ x ∈ D, b x = true

Unfolding `∀⟨v: D· b⟩`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_lam.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D b).ex ↔ ∃ x ∈ D, b x = true

theorem LaPToP.FunctionTheory.Fn.ex_lam.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D b).ex ↔
    ∃ x ∈ D, b x = true

Unfolding `∃⟨v: D· b⟩`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_top.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) :
  (LaPToP.FunctionTheory.Fn.lam D fun x =>
      LaPToP.BasicTheories.Binary.top).all

theorem LaPToP.FunctionTheory.Fn.all_top.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) :
  (LaPToP.FunctionTheory.Fn.lam D fun x =>
      LaPToP.BasicTheories.Binary.top).all

`∀v· ⊤` (Identity).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.not_ex_bot.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) :
  ¬(LaPToP.FunctionTheory.Fn.lam D fun x =>
        LaPToP.BasicTheories.Binary.bot).ex

theorem LaPToP.FunctionTheory.Fn.not_ex_bot.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) :
  ¬(LaPToP.FunctionTheory.Fn.lam D
        fun x =>
        LaPToP.BasicTheories.Binary.bot).ex

`¬∃v· ⊥` (Identity).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_const.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) (a : LaPToP.BasicTheories.Binary)
  (hD : Set.Nonempty D) :
  (LaPToP.FunctionTheory.Fn.lam D fun x => a).all ↔ a = true

theorem LaPToP.FunctionTheory.Fn.all_const.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (a : LaPToP.BasicTheories.Binary)
  (hD : Set.Nonempty D) :
  (LaPToP.FunctionTheory.Fn.lam D fun x =>
        a).all ↔
    a = true

`∀v: D· b = b` for `D ⧧ null` and `v` not in `b` (Idempotent).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_const.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) (a : LaPToP.BasicTheories.Binary)
  (hD : Set.Nonempty D) :
  (LaPToP.FunctionTheory.Fn.lam D fun x => a).ex ↔ a = true

theorem LaPToP.FunctionTheory.Fn.ex_const.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (a : LaPToP.BasicTheories.Binary)
  (hD : Set.Nonempty D) :
  (LaPToP.FunctionTheory.Fn.lam D fun x =>
        a).ex ↔
    a = true

`∃v: D· b = b` for `D ⧧ null` and `v` not in `b` (Idempotent).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.not_all.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  ¬(LaPToP.FunctionTheory.Fn.lam D b).all ↔
    (LaPToP.FunctionTheory.Fn.lam D fun v => !b v).ex

theorem LaPToP.FunctionTheory.Fn.not_all.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  ¬(LaPToP.FunctionTheory.Fn.lam D
          b).all ↔
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => !b v).ex

`¬∀v· b = ∃v· ¬b` (Duality).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.not_ex.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  ¬(LaPToP.FunctionTheory.Fn.lam D b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D fun v => !b v).all

theorem LaPToP.FunctionTheory.Fn.not_ex.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  ¬(LaPToP.FunctionTheory.Fn.lam D b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => !b v).all

`¬∃v· b = ∀v· ¬b` (Duality).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.and_all.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary) (hD : Set.Nonempty D) :
  a = true ∧ (LaPToP.FunctionTheory.Fn.lam D b).all ↔
    (LaPToP.FunctionTheory.Fn.lam D fun v => a && b v).all

theorem LaPToP.FunctionTheory.Fn.and_all.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary)
  (hD : Set.Nonempty D) :
  a = true ∧
      (LaPToP.FunctionTheory.Fn.lam D
          b).all ↔
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => a && b v).all

`a ∧ ∀v: D· b = ∀v: D· a ∧ b` for `D ⧧ null` (Distributive).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.and_ex.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary) :
  a = true ∧ (LaPToP.FunctionTheory.Fn.lam D b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D fun v => a && b v).ex

theorem LaPToP.FunctionTheory.Fn.and_ex.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary) :
  a = true ∧
      (LaPToP.FunctionTheory.Fn.lam D
          b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => a && b v).ex

`a ∧ ∃v: D· b = ∃v: D· a ∧ b` (Distributive; the book's proviso `D ⧧ null`
is not needed).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.or_all.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary) :
  a = true ∨ (LaPToP.FunctionTheory.Fn.lam D b).all ↔
    (LaPToP.FunctionTheory.Fn.lam D fun v => a || b v).all

theorem LaPToP.FunctionTheory.Fn.or_all.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary) :
  a = true ∨
      (LaPToP.FunctionTheory.Fn.lam D
          b).all ↔
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => a || b v).all

`a ∨ ∀v: D· b = ∀v: D· a ∨ b` (Distributive; the proviso is not needed).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.or_ex.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary) (hD : Set.Nonempty D) :
  a = true ∨ (LaPToP.FunctionTheory.Fn.lam D b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D fun v => a || b v).ex

theorem LaPToP.FunctionTheory.Fn.or_ex.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary)
  (hD : Set.Nonempty D) :
  a = true ∨
      (LaPToP.FunctionTheory.Fn.lam D
          b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => a || b v).ex

`a ∨ ∃v: D· b = ∃v: D· a ∨ b` for `D ⧧ null` (Distributive).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.imp_all.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary) :
  a = true → (LaPToP.FunctionTheory.Fn.lam D b).all ↔
    (LaPToP.FunctionTheory.Fn.lam D fun v => a.imp (b v)).all

theorem LaPToP.FunctionTheory.Fn.imp_all.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary) :
  a = true →
      (LaPToP.FunctionTheory.Fn.lam D
          b).all ↔
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => a.imp (b v)).all

`a ⇒ ∀v: D· b = ∀v: D· a ⇒ b` (Distributive; the proviso is not needed).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.imp_ex.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary) (hD : Set.Nonempty D) :
  a = true → (LaPToP.FunctionTheory.Fn.lam D b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D fun v => a.imp (b v)).ex

theorem LaPToP.FunctionTheory.Fn.imp_ex.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary)
  (hD : Set.Nonempty D) :
  a = true →
      (LaPToP.FunctionTheory.Fn.lam D
          b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => a.imp (b v)).ex

`a ⇒ ∃v: D· b = ∃v: D· a ⇒ b` for `D ⧧ null` (Distributive).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_imp.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D b).ex → a = true ↔
    (LaPToP.FunctionTheory.Fn.lam D fun v => a.rimp (b v)).all

theorem LaPToP.FunctionTheory.Fn.ex_imp.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D b).ex →
      a = true ↔
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => a.rimp (b v)).all

`a ⇐ ∃v: D· b = ∀v: D· a ⇐ b` (Antidistributive; the proviso is not needed).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_imp.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary) (hD : Set.Nonempty D) :
  (LaPToP.FunctionTheory.Fn.lam D b).all → a = true ↔
    (LaPToP.FunctionTheory.Fn.lam D fun v => a.rimp (b v)).ex

theorem LaPToP.FunctionTheory.Fn.all_imp.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (a : LaPToP.BasicTheories.Binary)
  (b : α → LaPToP.BasicTheories.Binary)
  (hD : Set.Nonempty D) :
  (LaPToP.FunctionTheory.Fn.lam D b).all →
      a = true ↔
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => a.rimp (b v)).ex

`a ⇐ ∀v: D· b = ∃v: D· a ⇐ b` for `D ⧧ null` (Antidistributive).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.apply_and_ex.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) (x : α) (hx : x ∈ D) :
  b x = true ∧ (LaPToP.FunctionTheory.Fn.lam D b).ex ↔ b x = true

theorem LaPToP.FunctionTheory.Fn.apply_and_ex.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary)
  (x : α) (hx : x ∈ D) :
  b x = true ∧
      (LaPToP.FunctionTheory.Fn.lam D
          b).ex ↔
    b x = true

`⟨v: D· b⟩ x ∧ ∃v: D· b = ⟨v: D· b⟩ x` for `x: D` (Absorption).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.apply_or_all.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) (x : α) (hx : x ∈ D) :
  b x = true ∨ (LaPToP.FunctionTheory.Fn.lam D b).all ↔ b x = true

theorem LaPToP.FunctionTheory.Fn.apply_or_all.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary)
  (x : α) (hx : x ∈ D) :
  b x = true ∨
      (LaPToP.FunctionTheory.Fn.lam D
          b).all ↔
    b x = true

`⟨v: D· b⟩ x ∨ ∀v: D· b = ⟨v: D· b⟩ x` for `x: D` (Absorption).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.apply_and_all.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) (x : α) (hx : x ∈ D) :
  b x = true ∧ (LaPToP.FunctionTheory.Fn.lam D b).all ↔
    (LaPToP.FunctionTheory.Fn.lam D b).all

theorem LaPToP.FunctionTheory.Fn.apply_and_all.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary)
  (x : α) (hx : x ∈ D) :
  b x = true ∧
      (LaPToP.FunctionTheory.Fn.lam D
          b).all ↔
    (LaPToP.FunctionTheory.Fn.lam D b).all

`⟨v: D· b⟩ x ∧ ∀v: D· b = ∀v: D· b` for `x: D` (Absorption).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.apply_or_ex.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) (x : α) (hx : x ∈ D) :
  b x = true ∨ (LaPToP.FunctionTheory.Fn.lam D b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D b).ex

theorem LaPToP.FunctionTheory.Fn.apply_or_ex.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary)
  (x : α) (hx : x ∈ D) :
  b x = true ∨
      (LaPToP.FunctionTheory.Fn.lam D
          b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D b).ex

`⟨v: D· b⟩ x ∨ ∃v: D· b = ∃v: D· b` for `x: D` (Absorption).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_and.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v => b v && c v).all ↔
    (LaPToP.FunctionTheory.Fn.lam D b).all ∧
      (LaPToP.FunctionTheory.Fn.lam D c).all

theorem LaPToP.FunctionTheory.Fn.all_and.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v =>
        b v && c v).all ↔
    (LaPToP.FunctionTheory.Fn.lam D
          b).all ∧
      (LaPToP.FunctionTheory.Fn.lam D
          c).all

`∀v· a ∧ b = (∀v· a) ∧ (∀v· b)` (Splitting).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_and.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v => b v && c v).ex →
    (LaPToP.FunctionTheory.Fn.lam D b).ex ∧
      (LaPToP.FunctionTheory.Fn.lam D c).ex

theorem LaPToP.FunctionTheory.Fn.ex_and.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v =>
        b v && c v).ex →
    (LaPToP.FunctionTheory.Fn.lam D
          b).ex ∧
      (LaPToP.FunctionTheory.Fn.lam D
          c).ex

`∃v· a ∧ b ⇒ (∃v· a) ∧ (∃v· b)` (Splitting).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_or.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D b).all ∨
      (LaPToP.FunctionTheory.Fn.lam D c).all →
    (LaPToP.FunctionTheory.Fn.lam D fun v => b v || c v).all

theorem LaPToP.FunctionTheory.Fn.all_or.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D b).all ∨
      (LaPToP.FunctionTheory.Fn.lam D
          c).all →
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => b v || c v).all

`∀v· a ∨ b ⇐ (∀v· a) ∨ (∀v· b)` (Splitting).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_or.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v => b v || c v).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D b).ex ∨
      (LaPToP.FunctionTheory.Fn.lam D c).ex

theorem LaPToP.FunctionTheory.Fn.ex_or.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v =>
        b v || c v).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D
          b).ex ∨
      (LaPToP.FunctionTheory.Fn.lam D
          c).ex

`∃v· a ∨ b = (∃v· a) ∨ (∃v· b)` (Splitting).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_imp_all.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v => (b v).imp (c v)).all →
    (LaPToP.FunctionTheory.Fn.lam D b).all →
      (LaPToP.FunctionTheory.Fn.lam D c).all

theorem LaPToP.FunctionTheory.Fn.all_imp_all.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v =>
        (b v).imp (c v)).all →
    (LaPToP.FunctionTheory.Fn.lam D
          b).all →
      (LaPToP.FunctionTheory.Fn.lam D
          c).all

`∀v· a ⇒ b ⇒ (∀v· a) ⇒ (∀v· b)` (Splitting).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_imp_ex.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v => (b v).imp (c v)).all →
    (LaPToP.FunctionTheory.Fn.lam D b).ex →
      (LaPToP.FunctionTheory.Fn.lam D c).ex

theorem LaPToP.FunctionTheory.Fn.all_imp_ex.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v =>
        (b v).imp (c v)).all →
    (LaPToP.FunctionTheory.Fn.lam D
          b).ex →
      (LaPToP.FunctionTheory.Fn.lam D
          c).ex

`∀v· a ⇒ b ⇒ (∃v· a) ⇒ (∃v· b)` (Splitting).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_beq_all.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v => b v == c v).all →
    ((LaPToP.FunctionTheory.Fn.lam D b).all ↔
      (LaPToP.FunctionTheory.Fn.lam D c).all)

theorem LaPToP.FunctionTheory.Fn.all_beq_all.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v =>
        b v == c v).all →
    ((LaPToP.FunctionTheory.Fn.lam D
          b).all ↔
      (LaPToP.FunctionTheory.Fn.lam D
          c).all)

`∀v· a = b ⇒ (∀v· a) = (∀v· b)` (Splitting).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_beq_ex.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v => b v == c v).all →
    ((LaPToP.FunctionTheory.Fn.lam D b).ex ↔
      (LaPToP.FunctionTheory.Fn.lam D c).ex)

theorem LaPToP.FunctionTheory.Fn.all_beq_ex.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D fun v =>
        b v == c v).all →
    ((LaPToP.FunctionTheory.Fn.lam D
          b).ex ↔
      (LaPToP.FunctionTheory.Fn.lam D
          c).ex)

`∀v· a = b ⇒ (∃v· a) = (∃v· b)` (Splitting).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.forall_forall_comm.{u} {α : Type u}
  (D E : LaPToP.BasicTheories.Bunch α) (q : α → α → Prop) :
  (∀ v ∈ D, ∀ w ∈ E, q v w) ↔ ∀ w ∈ E, ∀ v ∈ D, q v w

theorem LaPToP.FunctionTheory.Fn.forall_forall_comm.{u}
  {α : Type u}
  (D E : LaPToP.BasicTheories.Bunch α)
  (q : α → α → Prop) :
  (∀ v ∈ D, ∀ w ∈ E, q v w) ↔
    ∀ w ∈ E, ∀ v ∈ D, q v w

`∀v· ∀w· b = ∀w· ∀v· b` (Commutative), as iterated bounded quantification.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.exists_exists_comm.{u} {α : Type u}
  (D E : LaPToP.BasicTheories.Bunch α) (q : α → α → Prop) :
  (∃ v ∈ D, ∃ w ∈ E, q v w) ↔ ∃ w ∈ E, ∃ v ∈ D, q v w

theorem LaPToP.FunctionTheory.Fn.exists_exists_comm.{u}
  {α : Type u}
  (D E : LaPToP.BasicTheories.Bunch α)
  (q : α → α → Prop) :
  (∃ v ∈ D, ∃ w ∈ E, q v w) ↔
    ∃ w ∈ E, ∃ v ∈ D, q v w

`∃v· ∃w· b = ∃w· ∃v· b` (Commutative), as iterated bounded quantification.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.exists_forall_imp.{u} {α : Type u}
  (D E : LaPToP.BasicTheories.Bunch α) (q : α → α → Prop) :
  (∃ v ∈ D, ∀ w ∈ E, q v w) → ∀ w ∈ E, ∃ v ∈ D, q v w

theorem LaPToP.FunctionTheory.Fn.exists_forall_imp.{u}
  {α : Type u}
  (D E : LaPToP.BasicTheories.Bunch α)
  (q : α → α → Prop) :
  (∃ v ∈ D, ∀ w ∈ E, q v w) →
    ∀ w ∈ E, ∃ v ∈ D, q v w

`∃v· ∀w· b ⇒ ∀w· ∃v· b` (Semicommutative).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.forall_exists_iff_exists_fun.{u, v}
  {α : Type u} {β : Type v} (D : LaPToP.BasicTheories.Bunch α)
  [Nonempty β] (E : LaPToP.BasicTheories.Bunch β) (q : α → β → Prop) :
  (∀ x ∈ D, ∃ y ∈ E, q x y) ↔ ∃ f, ∀ x ∈ D, f x ∈ E ∧ q x (f x)

theorem LaPToP.FunctionTheory.Fn.forall_exists_iff_exists_fun.{u,
    v}
  {α : Type u} {β : Type v}
  (D : LaPToP.BasicTheories.Bunch α)
  [Nonempty β]
  (E : LaPToP.BasicTheories.Bunch β)
  (q : α → β → Prop) :
  (∀ x ∈ D, ∃ y ∈ E, q x y) ↔
    ∃ f, ∀ x ∈ D, f x ∈ E ∧ q x (f x)

`∀x· ∃y· p x y = ∃f· ∀x· p x (f x)` (Semicommutative): a choice function
for `x: D` into `E`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_image.{u, v} {α : Type u} {β : Type v}
  (b : α → LaPToP.BasicTheories.Binary) (g : β → α)
  (E : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.lam (g '' E) b).all ↔
    (LaPToP.FunctionTheory.Fn.lam E fun d => b (g d)).all

theorem LaPToP.FunctionTheory.Fn.all_image.{u, v}
  {α : Type u} {β : Type v}
  (b : α → LaPToP.BasicTheories.Binary)
  (g : β → α)
  (E : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.lam (g '' E)
        b).all ↔
    (LaPToP.FunctionTheory.Fn.lam E
        fun d => b (g d)).all

`∀r: f D· b = ∀d: D· ⟨r: f D· b⟩ (f d)` (Change of Variable).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_image.{u, v} {α : Type u} {β : Type v}
  (b : α → LaPToP.BasicTheories.Binary) (g : β → α)
  (E : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.lam (g '' E) b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam E fun d => b (g d)).ex

theorem LaPToP.FunctionTheory.Fn.ex_image.{u, v}
  {α : Type u} {β : Type v}
  (b : α → LaPToP.BasicTheories.Binary)
  (g : β → α)
  (E : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.lam (g '' E)
        b).ex ↔
    (LaPToP.FunctionTheory.Fn.lam E
        fun d => b (g d)).ex

`∃r: f D· b = ∃d: D· ⟨r: f D· b⟩ (f d)` (Change of Variable).

Proof for Theorem 3.11

uses 0

Unfold \forall\langle v : D \cdot b \rangle to \forall v \in D,\ b\,v = \top and reason propositionally; the nonempty domain supplies a witness where needed; the choice function of the last Semicommutative law is Classical.choose.

Theorem3.12

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Theorem 2.5

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsfunctionquantifierhehner-11.3.8

Laws of §11.3.8 for the solution quantifier and for domains: the \S-domain laws \forall v : (\S v : D \cdot b) \cdot c = \forall v : D \cdot b \Rightarrow c, \exists v : (\S v : D \cdot b) \cdot c = \exists v : D \cdot b \land c, \S v : (\S v : D \cdot b) \cdot c = \S v : D \cdot b \land c, \S v : A \mathbin{\lq} B \cdot b = (\S v : A \cdot b) \mathbin{\lq} (\S v : B \cdot b); Solution \S v : D \cdot \top = D, \S v : D \cdot \bot = \mathit{null}, (\S v \cdot b) : (\S v \cdot c) = \forall v \cdot b \Rightarrow c, (\S v \cdot b), (\S v \cdot c) = \S v \cdot b \lor c, (\S v \cdot b) \mathbin{\lq} (\S v \cdot c) = \S v \cdot b \land c, \forall f = ((\S f) = (\square f)), \exists f = ((\S f) \neq \mathit{null}); Inclusion A : B = \forall x : A \cdot x : B; Bunch-Element Conversion A : B = \forall a : A \cdot \exists b : B \cdot a = b and f\,A : g\,B = \forall a : A \cdot \exists b : B \cdot f\,a = g\,b; Domain Change A : B \Rightarrow (\forall v : A \cdot b) \Leftarrow (\forall v : B \cdot b), A : B \Rightarrow (\exists v : A \cdot b) \Rightarrow (\exists v : B \cdot b), \forall v : A \cdot v : B \Rightarrow p = \forall v : A \mathbin{\lq} B \cdot p, \exists v : A \cdot v : B \land p = \exists v : A \mathbin{\lq} B \cdot p. Uses Definition 3.6, Definition 3.5 and Theorem 2.5.

Lean code for Theorem3.12●19 theorems

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sols_lam.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D b).sols = {x | x ∈ D ∧ b x = true}

theorem LaPToP.FunctionTheory.Fn.sols_lam.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D
        b).sols =
    {x | x ∈ D ∧ b x = true}

Unfolding `§⟨v: D· b⟩`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_sols.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.FunctionTheory.Fn.lam D b).sols
        c).all ↔
    (LaPToP.FunctionTheory.Fn.lam D fun v => (b v).imp (c v)).all

theorem LaPToP.FunctionTheory.Fn.all_sols.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.FunctionTheory.Fn.lam D
            b).sols
        c).all ↔
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => (b v).imp (c v)).all

`∀v: (§v: D· b)· c = ∀v: D· b ⇒ c`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_sols.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.FunctionTheory.Fn.lam D b).sols
        c).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D fun v => b v && c v).ex

theorem LaPToP.FunctionTheory.Fn.ex_sols.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.FunctionTheory.Fn.lam D
            b).sols
        c).ex ↔
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => b v && c v).ex

`∃v: (§v: D· b)· c = ∃v: D· b ∧ c`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sols_sols.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (LaPToP.FunctionTheory.Fn.lam D b).sols
        c).sols =
    (LaPToP.FunctionTheory.Fn.lam D fun v => b v && c v).sols

theorem LaPToP.FunctionTheory.Fn.sols_sols.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam
        (LaPToP.FunctionTheory.Fn.lam D
            b).sols
        c).sols =
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => b v && c v).sols

`§v: (§v: D· b)· c = §v: D· b ∧ c`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sols_inter.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (A ∩ B) b).sols =
    (LaPToP.FunctionTheory.Fn.lam A b).sols ∩
      (LaPToP.FunctionTheory.Fn.lam B b).sols

theorem LaPToP.FunctionTheory.Fn.sols_inter.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam (A ∩ B)
        b).sols =
    (LaPToP.FunctionTheory.Fn.lam A
          b).sols ∩
      (LaPToP.FunctionTheory.Fn.lam B
          b).sols

`§v: A‘B· b = (§v: A· b) ‘ (§v: B· b)`.

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.subset_iff_all.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) [DecidablePred fun x => x ∈ B] :
  A ⊆ B ↔ (LaPToP.FunctionTheory.Fn.lam A fun v => decide (v ∈ B)).all

theorem LaPToP.FunctionTheory.Fn.subset_iff_all.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  [DecidablePred fun x => x ∈ B] :
  A ⊆ B ↔
    (LaPToP.FunctionTheory.Fn.lam A
        fun v => decide (v ∈ B)).all

`A: B = ∀x: A· x: B` (Inclusion).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.subset_iff_forall_exists.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A ⊆ B ↔ ∀ a ∈ A, ∃ b ∈ B, a = b

theorem LaPToP.FunctionTheory.Fn.subset_iff_forall_exists.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A ⊆ B ↔ ∀ a ∈ A, ∃ b ∈ B, a = b

`A: B = ∀a: A· ∃b: B· a = b` (Bunch-Element Conversion).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.image_subset_image_iff_forall_exists.{u, v}
  {α : Type u} {β : Type v} (f g : α → β)
  (A B : LaPToP.BasicTheories.Bunch α) :
  f '' A ⊆ g '' B ↔ ∀ a ∈ A, ∃ b ∈ B, f a = g b

theorem LaPToP.FunctionTheory.Fn.image_subset_image_iff_forall_exists.{u,
    v}
  {α : Type u} {β : Type v} (f g : α → β)
  (A B : LaPToP.BasicTheories.Bunch α) :
  f '' A ⊆ g '' B ↔
    ∀ a ∈ A, ∃ b ∈ B, f a = g b

`f A: g B = ∀a: A· ∃b: B· f a = g b` (Bunch-Element Conversion).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sols_top.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) :
  (LaPToP.FunctionTheory.Fn.lam D fun x =>
        LaPToP.BasicTheories.Binary.top).sols =
    D

theorem LaPToP.FunctionTheory.Fn.sols_top.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) :
  (LaPToP.FunctionTheory.Fn.lam D fun x =>
        LaPToP.BasicTheories.Binary.top).sols =
    D

`§v: D· ⊤ = D` (Solution).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sols_bot.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) :
  (LaPToP.FunctionTheory.Fn.lam D fun x =>
        LaPToP.BasicTheories.Binary.bot).sols =
    LaPToP.BasicTheories.Bunch.null

theorem LaPToP.FunctionTheory.Fn.sols_bot.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α) :
  (LaPToP.FunctionTheory.Fn.lam D fun x =>
        LaPToP.BasicTheories.Binary.bot).sols =
    LaPToP.BasicTheories.Bunch.null

`§v: D· ⊥ = null` (Solution).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sols_subset_sols.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D b).sols ⊆
      (LaPToP.FunctionTheory.Fn.lam D c).sols ↔
    (LaPToP.FunctionTheory.Fn.lam D fun v => (b v).imp (c v)).all

theorem LaPToP.FunctionTheory.Fn.sols_subset_sols.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D
          b).sols ⊆
      (LaPToP.FunctionTheory.Fn.lam D
          c).sols ↔
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => (b v).imp (c v)).all

`(§v· b): (§v· c) = ∀v· b ⇒ c` (Solution).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sols_union_sols.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D b).sols ∪
      (LaPToP.FunctionTheory.Fn.lam D c).sols =
    (LaPToP.FunctionTheory.Fn.lam D fun v => b v || c v).sols

theorem LaPToP.FunctionTheory.Fn.sols_union_sols.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D
          b).sols ∪
      (LaPToP.FunctionTheory.Fn.lam D
          c).sols =
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => b v || c v).sols

`(§v· b), (§v· c) = §v· b ∨ c` (Solution).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.sols_inter_sols.{u} {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c : α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D b).sols ∩
      (LaPToP.FunctionTheory.Fn.lam D c).sols =
    (LaPToP.FunctionTheory.Fn.lam D fun v => b v && c v).sols

theorem LaPToP.FunctionTheory.Fn.sols_inter_sols.{u}
  {α : Type u}
  (D : LaPToP.BasicTheories.Bunch α)
  (b c :
    α → LaPToP.BasicTheories.Binary) :
  (LaPToP.FunctionTheory.Fn.lam D
          b).sols ∩
      (LaPToP.FunctionTheory.Fn.lam D
          c).sols =
    (LaPToP.FunctionTheory.Fn.lam D
        fun v => b v && c v).sols

`(§v· b) ‘ (§v· c) = §v· b ∧ c` (Solution).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_iff_sols_eq_domain.{u} {α : Type u}
  (q : LaPToP.FunctionTheory.Pred α) :
  LaPToP.FunctionTheory.Fn.all q ↔
    LaPToP.FunctionTheory.Fn.sols q = LaPToP.FunctionTheory.Fn.domain q

theorem LaPToP.FunctionTheory.Fn.all_iff_sols_eq_domain.{u}
  {α : Type u}
  (q : LaPToP.FunctionTheory.Pred α) :
  LaPToP.FunctionTheory.Fn.all q ↔
    LaPToP.FunctionTheory.Fn.sols q =
      LaPToP.FunctionTheory.Fn.domain q

`∀f = ((§f) = (☐f))` (Solution).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_iff_sols_ne_null.{u} {α : Type u}
  (q : LaPToP.FunctionTheory.Pred α) :
  LaPToP.FunctionTheory.Fn.ex q ↔
    LaPToP.FunctionTheory.Fn.sols q ≠ LaPToP.BasicTheories.Bunch.null

theorem LaPToP.FunctionTheory.Fn.ex_iff_sols_ne_null.{u}
  {α : Type u}
  (q : LaPToP.FunctionTheory.Pred α) :
  LaPToP.FunctionTheory.Fn.ex q ↔
    LaPToP.FunctionTheory.Fn.sols q ≠
      LaPToP.BasicTheories.Bunch.null

`∃f = ((§f) ⧧ null)` (Solution).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_of_subset.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) (h : A ⊆ B) :
  (LaPToP.FunctionTheory.Fn.lam B b).all →
    (LaPToP.FunctionTheory.Fn.lam A b).all

theorem LaPToP.FunctionTheory.Fn.all_of_subset.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary)
  (h : A ⊆ B) :
  (LaPToP.FunctionTheory.Fn.lam B b).all →
    (LaPToP.FunctionTheory.Fn.lam A b).all

`A: B ⇒ (∀v: A· b) ⇐ (∀v: B· b)` (Domain Change).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_of_subset.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary) (h : A ⊆ B) :
  (LaPToP.FunctionTheory.Fn.lam A b).ex →
    (LaPToP.FunctionTheory.Fn.lam B b).ex

theorem LaPToP.FunctionTheory.Fn.ex_of_subset.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (b : α → LaPToP.BasicTheories.Binary)
  (h : A ⊆ B) :
  (LaPToP.FunctionTheory.Fn.lam A b).ex →
    (LaPToP.FunctionTheory.Fn.lam B b).ex

`A: B ⇒ (∃v: A· b) ⇒ (∃v: B· b)` (Domain Change).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.all_mem_imp.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (p : α → LaPToP.BasicTheories.Binary) [DecidablePred fun x => x ∈ B] :
  (LaPToP.FunctionTheory.Fn.lam A fun v =>
        LaPToP.BasicTheories.Binary.imp (decide (v ∈ B)) (p v)).all ↔
    (LaPToP.FunctionTheory.Fn.lam (A ∩ B) p).all

theorem LaPToP.FunctionTheory.Fn.all_mem_imp.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (p : α → LaPToP.BasicTheories.Binary)
  [DecidablePred fun x => x ∈ B] :
  (LaPToP.FunctionTheory.Fn.lam A fun v =>
        LaPToP.BasicTheories.Binary.imp
          (decide (v ∈ B)) (p v)).all ↔
    (LaPToP.FunctionTheory.Fn.lam (A ∩ B)
        p).all

`∀v: A· v: B ⇒ p = ∀v: A‘B· p` (Domain Change).

theoremdefined in LaPToP/FunctionTheory/Quantifiers.lean

complete

theorem LaPToP.FunctionTheory.Fn.ex_mem_and.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (p : α → LaPToP.BasicTheories.Binary) [DecidablePred fun x => x ∈ B] :
  (LaPToP.FunctionTheory.Fn.lam A fun v => decide (v ∈ B) && p v).ex ↔
    (LaPToP.FunctionTheory.Fn.lam (A ∩ B) p).ex

theorem LaPToP.FunctionTheory.Fn.ex_mem_and.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α)
  (p : α → LaPToP.BasicTheories.Binary)
  [DecidablePred fun x => x ∈ B] :
  (LaPToP.FunctionTheory.Fn.lam A fun v =>
        decide (v ∈ B) && p v).ex ↔
    (LaPToP.FunctionTheory.Fn.lam (A ∩ B)
        p).ex

`∃v: A· v: B ∧ p = ∃v: A‘B· p` (Domain Change).

Proof for Theorem 3.12

uses 0

Unfold \S\langle v : D \cdot b \rangle to \{v \mid v \in D \land b\,v = \top\} and reason by extensionality and propositional logic.

Definition3.13

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 3.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

"A union of functions applied to an argument gives the union of the results", (f, g)\,x = f\,x, g\,x, and "a function applied to a union of arguments gives the union of the results": f\,\mathit{null} = \mathit{null}, f\,(A, B) = f\,A, f\,B, f\,(\S g) = \S y : f\,(\square g) \cdot \exists x : \square g \cdot f\,x = y \land g\,x. "So function application distributes over bunch union. The range of function f is f\,(\square f)." In Lean Fn.applyBunch f A is the bunch of results of f on A : \square f, and Fn.applyFns F x applies a bunch of functions; the book's example \mathit{double}\,(2, 3) = 4, 6 is checked. Uses Theorem 3.2 and Definition 3.6.

Lean code for Definition3.13●11 declarations

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.applyBunch.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β)
  (A : LaPToP.BasicTheories.Bunch α) : LaPToP.BasicTheories.Bunch β

def LaPToP.FunctionTheory.Fn.applyBunch.{u, v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β)
  (A : LaPToP.BasicTheories.Bunch α) :
  LaPToP.BasicTheories.Bunch β

`f A`, a function applied to a bunch of arguments `A : ☐f`: the bunch of
results `f x` for `x : A`.

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.applyFns.{u, v} {α : Type u} {β : Type v}
  (F : LaPToP.BasicTheories.Bunch (LaPToP.FunctionTheory.Fn α β))
  (x : α) : LaPToP.BasicTheories.Bunch β

def LaPToP.FunctionTheory.Fn.applyFns.{u, v}
  {α : Type u} {β : Type v}
  (F :
    LaPToP.BasicTheories.Bunch
      (LaPToP.FunctionTheory.Fn α β))
  (x : α) : LaPToP.BasicTheories.Bunch β

`F x`, a bunch of functions applied to an argument: the bunch of results.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.applyBunch_null.{u, v} {α : Type u}
  {β : Type v} (f : LaPToP.FunctionTheory.Fn α β) :
  f.applyBunch LaPToP.BasicTheories.Bunch.null =
    LaPToP.BasicTheories.Bunch.null

theorem LaPToP.FunctionTheory.Fn.applyBunch_null.{u,
    v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) :
  f.applyBunch
      LaPToP.BasicTheories.Bunch.null =
    LaPToP.BasicTheories.Bunch.null

`f null = null`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.applyBunch_union.{u, v} {α : Type u}
  {β : Type v} (f : LaPToP.FunctionTheory.Fn α β)
  (A B : LaPToP.BasicTheories.Bunch α) :
  f.applyBunch (A ∪ B) = f.applyBunch A ∪ f.applyBunch B

theorem LaPToP.FunctionTheory.Fn.applyBunch_union.{u,
    v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β)
  (A B : LaPToP.BasicTheories.Bunch α) :
  f.applyBunch (A ∪ B) =
    f.applyBunch A ∪ f.applyBunch B

`f (A, B) = f A, f B`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.applyBunch_elem.{u, v} {α : Type u}
  {β : Type v} (f : LaPToP.FunctionTheory.Fn α β) (x : α)
  (h : x ∈ f.domain) :
  f.applyBunch (LaPToP.BasicTheories.Bunch.elem x) =
    LaPToP.BasicTheories.Bunch.elem (f.apply x h)

theorem LaPToP.FunctionTheory.Fn.applyBunch_elem.{u,
    v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β)
  (x : α) (h : x ∈ f.domain) :
  f.applyBunch
      (LaPToP.BasicTheories.Bunch.elem
        x) =
    LaPToP.BasicTheories.Bunch.elem
      (f.apply x h)

`f x = f x`: applied to an elementary bunch, `f` gives the elementary
result (the Application Axiom in bunch form).

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.values_eq_applyBunch_domain.{u, v} {α : Type u}
  {β : Type v} (f : LaPToP.FunctionTheory.Fn α β) :
  f.values = f.applyBunch f.domain

theorem LaPToP.FunctionTheory.Fn.values_eq_applyBunch_domain.{u,
    v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) :
  f.values = f.applyBunch f.domain

"The range of function `f` is `f (☐f)`."

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.applyBunch_sols.{u, v} {α : Type u}
  {β : Type v} (f : LaPToP.FunctionTheory.Fn α β)
  (g : LaPToP.FunctionTheory.Pred α)
  (hg : LaPToP.FunctionTheory.Fn.domain g ⊆ f.domain) :
  f.applyBunch (LaPToP.FunctionTheory.Fn.sols g) =
    {y |
      y ∈ f.applyBunch (LaPToP.FunctionTheory.Fn.domain g) ∧
        ∃ x,
          ∃ (h : x ∈ LaPToP.FunctionTheory.Fn.domain g),
            f.apply x ⋯ = y ∧
              LaPToP.FunctionTheory.Fn.apply g x h = true}

theorem LaPToP.FunctionTheory.Fn.applyBunch_sols.{u,
    v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β)
  (g : LaPToP.FunctionTheory.Pred α)
  (hg :
    LaPToP.FunctionTheory.Fn.domain g ⊆
      f.domain) :
  f.applyBunch
      (LaPToP.FunctionTheory.Fn.sols g) =
    {y |
      y ∈
          f.applyBunch
            (LaPToP.FunctionTheory.Fn.domain
              g) ∧
        ∃ x,
          ∃ (h :
            x ∈
              LaPToP.FunctionTheory.Fn.domain
                g),
            f.apply x ⋯ = y ∧
              LaPToP.FunctionTheory.Fn.apply
                  g x h =
                true}

`f (§g) = §y: f (☐g)· ∃x: ☐g· f x = y ∧ g x`, for a predicate `g` with
`☐g : ☐f` (the solution quantifier written as set-builder notation).

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.applyFns_union.{u, v} {α : Type u} {β : Type v}
  (x : α)
  (F G : LaPToP.BasicTheories.Bunch (LaPToP.FunctionTheory.Fn α β)) :
  LaPToP.FunctionTheory.Fn.applyFns (F ∪ G) x =
    LaPToP.FunctionTheory.Fn.applyFns F x ∪
      LaPToP.FunctionTheory.Fn.applyFns G x

theorem LaPToP.FunctionTheory.Fn.applyFns_union.{u,
    v}
  {α : Type u} {β : Type v} (x : α)
  (F G :
    LaPToP.BasicTheories.Bunch
      (LaPToP.FunctionTheory.Fn α β)) :
  LaPToP.FunctionTheory.Fn.applyFns
      (F ∪ G) x =
    LaPToP.FunctionTheory.Fn.applyFns F
        x ∪
      LaPToP.FunctionTheory.Fn.applyFns G
        x

`(f, g) x = f x, g x`: a union of functions applied to an argument gives
the union of the results.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.applyFns_elem.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) (x : α) (h : x ∈ f.domain) :
  LaPToP.FunctionTheory.Fn.applyFns (LaPToP.BasicTheories.Bunch.elem f)
      x =
    LaPToP.BasicTheories.Bunch.elem (f.apply x h)

theorem LaPToP.FunctionTheory.Fn.applyFns_elem.{u,
    v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β)
  (x : α) (h : x ∈ f.domain) :
  LaPToP.FunctionTheory.Fn.applyFns
      (LaPToP.BasicTheories.Bunch.elem f)
      x =
    LaPToP.BasicTheories.Bunch.elem
      (f.apply x h)

An elementary bunch of functions applied to an argument gives the
elementary result.

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.double : LaPToP.FunctionTheory.Fn ℤ ℤ

def LaPToP.FunctionTheory.Fn.double :
  LaPToP.FunctionTheory.Fn ℤ ℤ

The book's example: `double = ⟨n: nat· n+n⟩` applied to `2, 3` gives `4, 6`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.double_two_three :
  LaPToP.FunctionTheory.Fn.double.applyBunch
      (LaPToP.BasicTheories.Bunch.elem 2 ∪
        LaPToP.BasicTheories.Bunch.elem 3) =
    LaPToP.BasicTheories.Bunch.elem 4 ∪
      LaPToP.BasicTheories.Bunch.elem 6

theorem LaPToP.FunctionTheory.Fn.double_two_three :
  LaPToP.FunctionTheory.Fn.double.applyBunch
      (LaPToP.BasicTheories.Bunch.elem 2 ∪
        LaPToP.BasicTheories.Bunch.elem
          3) =
    LaPToP.BasicTheories.Bunch.elem 4 ∪
      LaPToP.BasicTheories.Bunch.elem 6

`double (2, 3) = 4, 6`.

Definition3.14

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 2.12

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

For a function whose body is a bunch (Fn α (Bunch β)): "a function that sometimes produces no result is called partial; ... always produces at least one result, total; ... always produces at most one result, deterministic; ... sometimes produces more than one result, nondeterministic". An ordinary function is viewed as a bunch-valued one with elementary results (Fn.toBunch), and is total and deterministic. The book's examples \langle n : \mathit{nat} \cdot n, n+1 \rangle (total, nondeterministic; it maps 3 to 3, 4) and \langle n : \mathit{nat} \cdot 0,..n \rangle ("both partial and nondeterministic") are verified. Uses Definition 3.13 and Definition 2.12.

Lean code for Definition3.14●14 declarations

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.Total.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α (LaPToP.BasicTheories.Bunch β)) : Prop

def LaPToP.FunctionTheory.Fn.Total.{u, v}
  {α : Type u} {β : Type v}
  (f :
    LaPToP.FunctionTheory.Fn α
      (LaPToP.BasicTheories.Bunch β)) :
  Prop

A bunch-valued function is *total* when it always produces at least one result.

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.Partial.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α (LaPToP.BasicTheories.Bunch β)) : Prop

def LaPToP.FunctionTheory.Fn.Partial.{u, v}
  {α : Type u} {β : Type v}
  (f :
    LaPToP.FunctionTheory.Fn α
      (LaPToP.BasicTheories.Bunch β)) :
  Prop

A bunch-valued function is *partial* when it sometimes produces no result.

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.Deterministic.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α (LaPToP.BasicTheories.Bunch β)) : Prop

def LaPToP.FunctionTheory.Fn.Deterministic.{u,
    v}
  {α : Type u} {β : Type v}
  (f :
    LaPToP.FunctionTheory.Fn α
      (LaPToP.BasicTheories.Bunch β)) :
  Prop

A bunch-valued function is *deterministic* when it always produces at most one result.

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.Nondeterministic.{u, v} {α : Type u}
  {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α (LaPToP.BasicTheories.Bunch β)) : Prop

def LaPToP.FunctionTheory.Fn.Nondeterministic.{u,
    v}
  {α : Type u} {β : Type v}
  (f :
    LaPToP.FunctionTheory.Fn α
      (LaPToP.BasicTheories.Bunch β)) :
  Prop

A bunch-valued function is *nondeterministic* when it sometimes produces more than one result.

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.toBunch.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) :
  LaPToP.FunctionTheory.Fn α (LaPToP.BasicTheories.Bunch β)

def LaPToP.FunctionTheory.Fn.toBunch.{u, v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) :
  LaPToP.FunctionTheory.Fn α
    (LaPToP.BasicTheories.Bunch β)

An ordinary function viewed as a bunch-valued one: each result is an
elementary bunch.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.total_toBunch.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) : f.toBunch.Total

theorem LaPToP.FunctionTheory.Fn.total_toBunch.{u,
    v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) :
  f.toBunch.Total

An ordinary function is total.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.deterministic_toBunch.{u, v} {α : Type u}
  {β : Type v} (f : LaPToP.FunctionTheory.Fn α β) :
  f.toBunch.Deterministic

theorem LaPToP.FunctionTheory.Fn.deterministic_toBunch.{u,
    v}
  {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α β) :
  f.toBunch.Deterministic

An ordinary function is deterministic.

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.pair :
  LaPToP.FunctionTheory.Fn ℤ (LaPToP.BasicTheories.Bunch ℤ)

def LaPToP.FunctionTheory.Fn.pair :
  LaPToP.FunctionTheory.Fn ℤ
    (LaPToP.BasicTheories.Bunch ℤ)

`⟨n: nat· n, n+1⟩`, mapping each natural number to two natural numbers.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.pair_three :
  LaPToP.FunctionTheory.Fn.pair.apply 3 ⋯ =
    LaPToP.BasicTheories.Bunch.elem 3 ∪
      LaPToP.BasicTheories.Bunch.elem 4

theorem LaPToP.FunctionTheory.Fn.pair_three :
  LaPToP.FunctionTheory.Fn.pair.apply 3
      ⋯ =
    LaPToP.BasicTheories.Bunch.elem 3 ∪
      LaPToP.BasicTheories.Bunch.elem 4

`⟨n: nat· n, n+1⟩ 3 = 3, 4`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.total_pair :
  LaPToP.FunctionTheory.Fn.pair.Total

theorem LaPToP.FunctionTheory.Fn.total_pair :
  LaPToP.FunctionTheory.Fn.pair.Total

`⟨n: nat· n, n+1⟩` is total.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.nondeterministic_pair :
  LaPToP.FunctionTheory.Fn.pair.Nondeterministic

theorem LaPToP.FunctionTheory.Fn.nondeterministic_pair :
  LaPToP.FunctionTheory.Fn.pair.Nondeterministic

`⟨n: nat· n, n+1⟩` is nondeterministic.

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.below :
  LaPToP.FunctionTheory.Fn ℤ (LaPToP.BasicTheories.Bunch ℤ)

def LaPToP.FunctionTheory.Fn.below :
  LaPToP.FunctionTheory.Fn ℤ
    (LaPToP.BasicTheories.Bunch ℤ)

`⟨n: nat· 0,..n⟩`, "both partial and nondeterministic".

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.partial_below :
  LaPToP.FunctionTheory.Fn.below.Partial

theorem LaPToP.FunctionTheory.Fn.partial_below :
  LaPToP.FunctionTheory.Fn.below.Partial

`⟨n: nat· 0,..n⟩` is partial: at `0` it produces no result.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.nondeterministic_below :
  LaPToP.FunctionTheory.Fn.below.Nondeterministic

theorem LaPToP.FunctionTheory.Fn.nondeterministic_below :
  LaPToP.FunctionTheory.Fn.below.Nondeterministic

`⟨n: nat· 0,..n⟩` is nondeterministic: at `2` it produces `0` and `1`.

Theorem3.15

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 4

Statement dependency previews

Preview

Theorem 2.11

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsfunctionhehner-3.2

The Function Inclusion Law f : g = \square f :: \square g \land \forall x : \square g \cdot f\,x : g\,x, and, "using it both ways round", function equality f = g = \square f = \square g \land \forall x : \square f \cdot f\,x = g\,x. A \to B abbreviates \langle n : A \cdot B \rangle, "a nondeterministic function whose result, for each element of its domain A, is the bunch B"; "it is also the bunch of all functions whose domain includes A and whose result is included in B" — both readings are defined (Fn.arrowB, Fn.arrowSet) and shown to agree. Laws: f : A \to B = \square f :: A \land f\,A : B; the Arrow laws of §11.3.7 f : \mathit{null} \to A, (A, B) \to (C \mathbin{\lq} D) : A \to C : (A \mathbin{\lq} B) \to (C, D), (A, B) \to C = A \to C \mid B \to C, and A \to B : C \to D = A :: C \land B : D corrected: the second conjunct is needed only when C \neq \mathit{null} (for C = \mathit{null} the inclusion holds vacuously, since f : \mathit{null} \to D for every f). The book's worked inclusions \mathit{suc} : \mathit{nat} \to \mathit{nat}, \mathit{even} : \mathit{int} \to \mathit{bin}, \mathit{odd} : \mathit{int} \to \mathit{bin}, \mathit{divides} : (\mathit{nat}+1) \to \mathit{int} \to \mathit{bin} are proved. Uses Definition 3.14, Definition 3.3, Definition 3.4 and Theorem 2.11.

Lean code for Theorem3.15●20 declarations

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.Incl.{u, v} {α : Type u} {β : Type v}
  (f g : LaPToP.FunctionTheory.Fn α (LaPToP.BasicTheories.Bunch β)) :
  Prop

def LaPToP.FunctionTheory.Fn.Incl.{u, v}
  {α : Type u} {β : Type v}
  (f g :
    LaPToP.FunctionTheory.Fn α
      (LaPToP.BasicTheories.Bunch β)) :
  Prop

`f: g`, the Function Inclusion Law: `☐f :: ☐g ∧ ∀x: ☐g· f x : g x`.

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.arrowB.{u, v} {α : Type u} {β : Type v}
  (A : LaPToP.BasicTheories.Bunch α)
  (B : LaPToP.BasicTheories.Bunch β) :
  LaPToP.FunctionTheory.Fn α (LaPToP.BasicTheories.Bunch β)

def LaPToP.FunctionTheory.Fn.arrowB.{u, v}
  {α : Type u} {β : Type v}
  (A : LaPToP.BasicTheories.Bunch α)
  (B : LaPToP.BasicTheories.Bunch β) :
  LaPToP.FunctionTheory.Fn α
    (LaPToP.BasicTheories.Bunch β)

`A→B` as a function: `⟨n: A· B⟩`, the nondeterministic function whose
result, for each element of `A`, is the bunch `B`.

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.arrowSet.{u, v} {α : Type u} {β : Type v}
  (A : LaPToP.BasicTheories.Bunch α)
  (B : LaPToP.BasicTheories.Bunch β) :
  LaPToP.BasicTheories.Bunch (LaPToP.FunctionTheory.Fn α β)

def LaPToP.FunctionTheory.Fn.arrowSet.{u, v}
  {α : Type u} {β : Type v}
  (A : LaPToP.BasicTheories.Bunch α)
  (B : LaPToP.BasicTheories.Bunch β) :
  LaPToP.BasicTheories.Bunch
    (LaPToP.FunctionTheory.Fn α β)

`A→B` as a bunch of functions: "the bunch of all functions whose domain
includes `A` and whose result is included in `B`".

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.eq_iff.{u, v} {α : Type u} {β : Type v}
  (f g : LaPToP.FunctionTheory.Fn α β) :
  f = g ↔
    f.domain = g.domain ∧
      ∀ (x : α) (hf : x ∈ f.domain) (hg : x ∈ g.domain),
        f.apply x hf = g.apply x hg

theorem LaPToP.FunctionTheory.Fn.eq_iff.{u, v}
  {α : Type u} {β : Type v}
  (f g : LaPToP.FunctionTheory.Fn α β) :
  f = g ↔
    f.domain = g.domain ∧
      ∀ (x : α) (hf : x ∈ f.domain)
        (hg : x ∈ g.domain),
        f.apply x hf = g.apply x hg

`f = g = ☐f = ☐g ∧ ∀x: ☐f· f x = g x` (function equality).

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.incl_antisymm.{u, v} {α : Type u} {β : Type v}
  (f g : LaPToP.FunctionTheory.Fn α (LaPToP.BasicTheories.Bunch β))
  (h₁ : f.Incl g) (h₂ : g.Incl f) : f = g

theorem LaPToP.FunctionTheory.Fn.incl_antisymm.{u,
    v}
  {α : Type u} {β : Type v}
  (f g :
    LaPToP.FunctionTheory.Fn α
      (LaPToP.BasicTheories.Bunch β))
  (h₁ : f.Incl g) (h₂ : g.Incl f) : f = g

Function inclusion both ways round is function equality.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.incl_refl.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α (LaPToP.BasicTheories.Bunch β)) :
  f.Incl f

theorem LaPToP.FunctionTheory.Fn.incl_refl.{u, v}
  {α : Type u} {β : Type v}
  (f :
    LaPToP.FunctionTheory.Fn α
      (LaPToP.BasicTheories.Bunch β)) :
  f.Incl f

`f: f` (reflexivity of function inclusion).

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.incl_arrowB.{u, v} {α : Type u} {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α (LaPToP.BasicTheories.Bunch β))
  (A : LaPToP.BasicTheories.Bunch α)
  (B : LaPToP.BasicTheories.Bunch β) :
  f.Incl (LaPToP.FunctionTheory.Fn.arrowB A B) ↔
    A ⊆ f.dom ∧ ∀ x ∈ A, ∀ (hf : x ∈ f.dom), f.apply x hf ⊆ B

theorem LaPToP.FunctionTheory.Fn.incl_arrowB.{u,
    v}
  {α : Type u} {β : Type v}
  (f :
    LaPToP.FunctionTheory.Fn α
      (LaPToP.BasicTheories.Bunch β))
  (A : LaPToP.BasicTheories.Bunch α)
  (B : LaPToP.BasicTheories.Bunch β) :
  f.Incl
      (LaPToP.FunctionTheory.Fn.arrowB A
        B) ↔
    A ⊆ f.dom ∧
      ∀ x ∈ A,
        ∀ (hf : x ∈ f.dom),
          f.apply x hf ⊆ B

`f: A→B = ☐f :: A ∧ f A : B`: the results of `f` on `A` are included in `B`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.mem_arrowSet_iff.{u, v} {α : Type u}
  {β : Type v} (A : LaPToP.BasicTheories.Bunch α)
  (B : LaPToP.BasicTheories.Bunch β)
  (g : LaPToP.FunctionTheory.Fn α β) :
  g ∈ LaPToP.FunctionTheory.Fn.arrowSet A B ↔
    A ⊆ g.dom ∧ g.applyBunch A ⊆ B

theorem LaPToP.FunctionTheory.Fn.mem_arrowSet_iff.{u,
    v}
  {α : Type u} {β : Type v}
  (A : LaPToP.BasicTheories.Bunch α)
  (B : LaPToP.BasicTheories.Bunch β)
  (g : LaPToP.FunctionTheory.Fn α β) :
  g ∈
      LaPToP.FunctionTheory.Fn.arrowSet A
        B ↔
    A ⊆ g.dom ∧ g.applyBunch A ⊆ B

`g: A→B` for an ordinary function `g`: `☐g :: A ∧ g A : B`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.incl_toBunch_arrowB_iff.{u, v} {α : Type u}
  {β : Type v} (A : LaPToP.BasicTheories.Bunch α)
  (B : LaPToP.BasicTheories.Bunch β)
  (g : LaPToP.FunctionTheory.Fn α β) :
  g.toBunch.Incl (LaPToP.FunctionTheory.Fn.arrowB A B) ↔
    g ∈ LaPToP.FunctionTheory.Fn.arrowSet A B

theorem LaPToP.FunctionTheory.Fn.incl_toBunch_arrowB_iff.{u,
    v}
  {α : Type u} {β : Type v}
  (A : LaPToP.BasicTheories.Bunch α)
  (B : LaPToP.BasicTheories.Bunch β)
  (g : LaPToP.FunctionTheory.Fn α β) :
  g.toBunch.Incl
      (LaPToP.FunctionTheory.Fn.arrowB A
        B) ↔
    g ∈
      LaPToP.FunctionTheory.Fn.arrowSet A
        B

The two readings of `A→B` agree: `g: A→B` as inclusion of `g` in the
function `A→B` is membership of `g` in the bunch `A→B`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.incl_arrowB_null.{u, v} {α : Type u}
  {β : Type v}
  (f : LaPToP.FunctionTheory.Fn α (LaPToP.BasicTheories.Bunch β))
  (B : LaPToP.BasicTheories.Bunch β) :
  f.Incl
    (LaPToP.FunctionTheory.Fn.arrowB LaPToP.BasicTheories.Bunch.null B)

theorem LaPToP.FunctionTheory.Fn.incl_arrowB_null.{u,
    v}
  {α : Type u} {β : Type v}
  (f :
    LaPToP.FunctionTheory.Fn α
      (LaPToP.BasicTheories.Bunch β))
  (B : LaPToP.BasicTheories.Bunch β) :
  f.Incl
    (LaPToP.FunctionTheory.Fn.arrowB
      LaPToP.BasicTheories.Bunch.null B)

`f: null→A` (Arrow).

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.arrowB_incl_arrowB.{u, v} {α : Type u}
  {β : Type v} (A C : LaPToP.BasicTheories.Bunch α)
  (B D : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.arrowB A B).Incl
      (LaPToP.FunctionTheory.Fn.arrowB C D) ↔
    C ⊆ A ∧ (Set.Nonempty C → B ⊆ D)

theorem LaPToP.FunctionTheory.Fn.arrowB_incl_arrowB.{u,
    v}
  {α : Type u} {β : Type v}
  (A C : LaPToP.BasicTheories.Bunch α)
  (B D : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.arrowB A
          B).Incl
      (LaPToP.FunctionTheory.Fn.arrowB C
        D) ↔
    C ⊆ A ∧ (Set.Nonempty C → B ⊆ D)

`A→B : C→D = A::C ∧ B:D` (Arrow), corrected: the second conjunct is needed
only when `C ⧧ null` (for `C = null` the inclusion holds vacuously).

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.arrowB_union_inter_incl.{u, v} {α : Type u}
  {β : Type v} (A C : LaPToP.BasicTheories.Bunch α)
  (B D : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.arrowB (A ∪ C) (B ∩ D)).Incl
    (LaPToP.FunctionTheory.Fn.arrowB A B)

theorem LaPToP.FunctionTheory.Fn.arrowB_union_inter_incl.{u,
    v}
  {α : Type u} {β : Type v}
  (A C : LaPToP.BasicTheories.Bunch α)
  (B D : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.arrowB (A ∪ C)
        (B ∩ D)).Incl
    (LaPToP.FunctionTheory.Fn.arrowB A B)

`(A, B)→(C‘D) : A→C` (Arrow).

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.arrowB_incl_inter_union.{u, v} {α : Type u}
  {β : Type v} (A C : LaPToP.BasicTheories.Bunch α)
  (B D : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.arrowB A B).Incl
    (LaPToP.FunctionTheory.Fn.arrowB (A ∩ C) (B ∪ D))

theorem LaPToP.FunctionTheory.Fn.arrowB_incl_inter_union.{u,
    v}
  {α : Type u} {β : Type v}
  (A C : LaPToP.BasicTheories.Bunch α)
  (B D : LaPToP.BasicTheories.Bunch β) :
  (LaPToP.FunctionTheory.Fn.arrowB A
        B).Incl
    (LaPToP.FunctionTheory.Fn.arrowB
      (A ∩ C) (B ∪ D))

`A→C : (A‘B)→(C, D)` (Arrow).

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.arrowB_union_eq_orElse.{u, v} {α : Type u}
  {β : Type v} (A C : LaPToP.BasicTheories.Bunch α)
  (B : LaPToP.BasicTheories.Bunch β) :
  LaPToP.FunctionTheory.Fn.arrowB (A ∪ C) B =
    (LaPToP.FunctionTheory.Fn.arrowB A B).orElse
      (LaPToP.FunctionTheory.Fn.arrowB C B)

theorem LaPToP.FunctionTheory.Fn.arrowB_union_eq_orElse.{u,
    v}
  {α : Type u} {β : Type v}
  (A C : LaPToP.BasicTheories.Bunch α)
  (B : LaPToP.BasicTheories.Bunch β) :
  LaPToP.FunctionTheory.Fn.arrowB (A ∪ C)
      B =
    (LaPToP.FunctionTheory.Fn.arrowB A
          B).orElse
      (LaPToP.FunctionTheory.Fn.arrowB C
        B)

`(A, B)→C = A→C | B→C` (Arrow).

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.FunctionTheory.Fn.suc : LaPToP.FunctionTheory.Fn ℤ ℤ

def LaPToP.FunctionTheory.Fn.suc :
  LaPToP.FunctionTheory.Fn ℤ ℤ

`suc = ⟨n: nat· n+1⟩`, the successor function on the natural numbers.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.suc_three :
  LaPToP.FunctionTheory.Fn.suc.apply 3 ⋯ = 4

theorem LaPToP.FunctionTheory.Fn.suc_three :
  LaPToP.FunctionTheory.Fn.suc.apply 3 ⋯ =
    4

`suc 3 = 4`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.suc_incl :
  LaPToP.FunctionTheory.Fn.suc ∈
    LaPToP.FunctionTheory.Fn.arrowSet LaPToP.BasicTheories.Bunch.nat
      LaPToP.BasicTheories.Bunch.nat

theorem LaPToP.FunctionTheory.Fn.suc_incl :
  LaPToP.FunctionTheory.Fn.suc ∈
    LaPToP.FunctionTheory.Fn.arrowSet
      LaPToP.BasicTheories.Bunch.nat
      LaPToP.BasicTheories.Bunch.nat

`suc: nat→nat`, the book's worked proof by the Function Inclusion Law.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.even_incl :
  LaPToP.FunctionTheory.even ∈
    LaPToP.FunctionTheory.Fn.arrowSet LaPToP.BasicTheories.Bunch.int
      LaPToP.BasicTheories.Bunch.bin

theorem LaPToP.FunctionTheory.Fn.even_incl :
  LaPToP.FunctionTheory.even ∈
    LaPToP.FunctionTheory.Fn.arrowSet
      LaPToP.BasicTheories.Bunch.int
      LaPToP.BasicTheories.Bunch.bin

`even: int→bin`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.odd_incl :
  LaPToP.FunctionTheory.odd ∈
    LaPToP.FunctionTheory.Fn.arrowSet LaPToP.BasicTheories.Bunch.int
      LaPToP.BasicTheories.Bunch.bin

theorem LaPToP.FunctionTheory.Fn.odd_incl :
  LaPToP.FunctionTheory.odd ∈
    LaPToP.FunctionTheory.Fn.arrowSet
      LaPToP.BasicTheories.Bunch.int
      LaPToP.BasicTheories.Bunch.bin

`odd: int→bin`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.FunctionTheory.Fn.divides_incl :
  LaPToP.FunctionTheory.divides ∈
    LaPToP.FunctionTheory.Fn.arrowSet
      (LaPToP.BasicTheories.Bunch.nat +
        LaPToP.BasicTheories.Bunch.elem 1)
      (LaPToP.FunctionTheory.Fn.arrowSet LaPToP.BasicTheories.Bunch.int
        LaPToP.BasicTheories.Bunch.bin)

theorem LaPToP.FunctionTheory.Fn.divides_incl :
  LaPToP.FunctionTheory.divides ∈
    LaPToP.FunctionTheory.Fn.arrowSet
      (LaPToP.BasicTheories.Bunch.nat +
        LaPToP.BasicTheories.Bunch.elem 1)
      (LaPToP.FunctionTheory.Fn.arrowSet
        LaPToP.BasicTheories.Bunch.int
        LaPToP.BasicTheories.Bunch.bin)

`divides: (nat+1)→int→bin`.

Proof for Theorem 3.15

uses 0

Unfolding; equality via Fn.ext; \mathit{suc} : \mathit{nat} \to \mathit{nat} by the construction axiom 0 \le n \Rightarrow 0 \le n+1.

Theorem3.16

Group member previews

Preview

Definition 3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 4

Statement dependency previews

Preview

Theorem 3.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

EffortsmallTagsfunctionlisthehner-3.3

"A list L has much in common with the function \langle n : \square L \cdot L\,n \rangle": list indexing is function application L\,m = \langle n : \square L \cdot L\,n \rangle\,m; list composition coincides with function composition L\,M\,m = \langle n : \square L \cdot L\,n \rangle\,\langle n : \square M \cdot M\,n \rangle\,m; list domain and size are function domain and size; list equality is function equality; quantifiers apply to lists, \Sigma L = \Sigma n : \square L \cdot L\,n. Functions compose with lists (\mathit{suc}\,[3; 5; 2] = [4; 6; 3], -[3; 5; 2] = [-3; -5; -2]), and lists and functions mix in a selective union: 1 \to 21 \mid [10; 11; 12] = [10; 21; 12], in general n \to i \mid L = (n \to i \mid L) for an index n of L. Uses Definition 4.9, Theorem 3.2, Definition 3.3 and Definition 3.8.

Lean code for Theorem3.16●12 declarations

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.DataStructures.HList.toFn.{u} {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α) : LaPToP.FunctionTheory.Fn ℕ α

def LaPToP.DataStructures.HList.toFn.{u}
  {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α) :
  LaPToP.FunctionTheory.Fn ℕ α

`⟨n: ☐L· L n⟩`, a list viewed as a function on its domain.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.DataStructures.HList.toFn_apply.{u} {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α) (m : ℕ) (h : m ∈ L.domain) :
  L.toFn.apply m h = L.at m

theorem LaPToP.DataStructures.HList.toFn_apply.{u}
  {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α)
  (m : ℕ) (h : m ∈ L.domain) :
  L.toFn.apply m h = L.at m

`L m = ⟨n: ☐L· L n⟩ m`: list indexing is function application.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.DataStructures.HList.toFn_domain.{u} {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α) : L.toFn.domain = L.domain

theorem LaPToP.DataStructures.HList.toFn_domain.{u}
  {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α) :
  L.toFn.domain = L.domain

`☐L = ☐⟨n: ☐L· L n⟩`: list domain is function domain.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.DataStructures.HList.toFn_size.{u} {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α) : L.toFn.size = L.length

theorem LaPToP.DataStructures.HList.toFn_size.{u}
  {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α) :
  L.toFn.size = L.length

`#L = #⟨n: ☐L· L n⟩`: list size is function size.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.DataStructures.HList.toFn_comp.{u} {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α) (m : ℕ)
  (N : LaPToP.DataStructures.HList ℕ) (hm : m ∈ N.domain)
  (hL : N.at m ∈ L.domain) :
  (L.comp N).toFn.apply m ⋯ = L.toFn.apply (N.toFn.apply m hm) hL

theorem LaPToP.DataStructures.HList.toFn_comp.{u}
  {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α)
  (m : ℕ)
  (N : LaPToP.DataStructures.HList ℕ)
  (hm : m ∈ N.domain)
  (hL : N.at m ∈ L.domain) :
  (L.comp N).toFn.apply m ⋯ =
    L.toFn.apply (N.toFn.apply m hm) hL

`L M m = ⟨n: ☐L· L n⟩ ⟨n: ☐M· M n⟩ m`: list composition is function
composition, for `m` an index of `M` whose item is an index of `L`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.DataStructures.HList.toFn_inj.{u} {α : Type u} [Inhabited α]
  (L M : LaPToP.DataStructures.HList α) : L.toFn = M.toFn ↔ L = M

theorem LaPToP.DataStructures.HList.toFn_inj.{u}
  {α : Type u} [Inhabited α]
  (L M : LaPToP.DataStructures.HList α) :
  L.toFn = M.toFn ↔ L = M

`L = M = ⟨n: ☐L· L n⟩ = ⟨n: ☐M· M n⟩`: list equality is function equality.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.DataStructures.HList.sum_toFn
  (L : LaPToP.DataStructures.HList LaPToP.BasicTheories.Number) :
  L.toFn.sum = List.sum L.contents

theorem LaPToP.DataStructures.HList.sum_toFn
  (L :
    LaPToP.DataStructures.HList
      LaPToP.BasicTheories.Number) :
  L.toFn.sum = List.sum L.contents

`ΣL = Σn: ☐L· L n`: the sum of the items of a list of numbers.

defdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

def LaPToP.DataStructures.HList.map.{u, v} {α : Type u} {β : Type v}
  (f : α → β) (L : LaPToP.DataStructures.HList α) :
  LaPToP.DataStructures.HList β

def LaPToP.DataStructures.HList.map.{u, v}
  {α : Type u} {β : Type v} (f : α → β)
  (L : LaPToP.DataStructures.HList α) :
  LaPToP.DataStructures.HList β

A function composed with a list: `f L` applies `f` to each item.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.DataStructures.HList.suc_map_example :
  LaPToP.DataStructures.HList.map (fun x => x + 1)
      (LaPToP.DataStructures.Str.pack [3, 5, 2]) =
    LaPToP.DataStructures.Str.pack [4, 6, 3]

theorem LaPToP.DataStructures.HList.suc_map_example :
  LaPToP.DataStructures.HList.map
      (fun x => x + 1)
      (LaPToP.DataStructures.Str.pack
        [3, 5, 2]) =
    LaPToP.DataStructures.Str.pack
      [4, 6, 3]

`suc [3; 5; 2] = [4; 6; 3]`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.DataStructures.HList.neg_map_example :
  LaPToP.DataStructures.HList.map Neg.neg
      (LaPToP.DataStructures.Str.pack [3, 5, 2]) =
    LaPToP.DataStructures.Str.pack [-3, -5, -2]

theorem LaPToP.DataStructures.HList.neg_map_example :
  LaPToP.DataStructures.HList.map Neg.neg
      (LaPToP.DataStructures.Str.pack
        [3, 5, 2]) =
    LaPToP.DataStructures.Str.pack
      [-3, -5, -2]

`–[3; 5; 2] = [–3; –5; –2]`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.DataStructures.HList.orElse_arrow_toFn.{u} {α : Type u}
  [Inhabited α] (L : LaPToP.DataStructures.HList α) (n : ℕ) (i : α)
  (hn : n ∈ L.domain) :
  (LaPToP.FunctionTheory.Fn.arrow n i).orElse L.toFn =
    (LaPToP.DataStructures.HList.modify n i L).toFn

theorem LaPToP.DataStructures.HList.orElse_arrow_toFn.{u}
  {α : Type u} [Inhabited α]
  (L : LaPToP.DataStructures.HList α)
  (n : ℕ) (i : α) (hn : n ∈ L.domain) :
  (LaPToP.FunctionTheory.Fn.arrow n
          i).orElse
      L.toFn =
    (LaPToP.DataStructures.HList.modify n
        i L).toFn

`n→i | L = (n→i | L)`: a selective union of an arrow and a list is the
modified list, for `n` an index of `L`.

theoremdefined in LaPToP/FunctionTheory/FinePoints.lean

complete

theorem LaPToP.DataStructures.HList.orElse_arrow_example :
  (LaPToP.FunctionTheory.Fn.arrow 1 21).orElse
      (LaPToP.DataStructures.Str.pack [10, 11, 12]).toFn =
    (LaPToP.DataStructures.Str.pack [10, 21, 12]).toFn

theorem LaPToP.DataStructures.HList.orElse_arrow_example :
  (LaPToP.FunctionTheory.Fn.arrow 1
          21).orElse
      (LaPToP.DataStructures.Str.pack
          [10, 11, 12]).toFn =
    (LaPToP.DataStructures.Str.pack
        [10, 21, 12]).toFn

`1→21 | [10; 11; 12] = [10; 21; 12]`, the book's example.

Proof for Theorem 3.16

uses 0

HList.toFn L := ⟨n: ☐L· L n⟩; the coincidences are rfl or Fn.ext; size via Finset.range; \Sigma L via Fin.sum_univ_getElem; the selective-union law by extensionality and List.getElem?_set_self/_ne.