Mathlib.Order.CompleteBooleanAlgebra

Order.Frame.MinimalAxioms structure

(α : Type u) extends CompleteLattice α

Full source

/-- Structure containing the minimal axioms required to check that an order is a frame. Do NOT use,
except for implementing `Order.Frame` via `Order.Frame.ofMinimalAxioms`.

This structure omits the `himp`, `compl` fields, which can be recovered using
`Order.Frame.ofMinimalAxioms`. -/
class Order.Frame.MinimalAxioms (α : Type u) extends CompleteLattice α where
  inf_sSup_le_iSup_inf (a : α) (s : Set α) : a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

Minimal Frame Axioms

Informal description

A structure containing the minimal axioms required to verify that a complete lattice $\alpha$ satisfies the frame property, namely that finite meets distribute over arbitrary joins. This structure is used as an intermediate step in constructing a full frame structure, which additionally includes the `himp` and `compl` operations.

Order.Coframe.MinimalAxioms structure

(α : Type u) extends CompleteLattice α

Full source

/-- Structure containing the minimal axioms required to check that an order is a coframe. Do NOT
use, except for implementing `Order.Coframe` via `Order.Coframe.ofMinimalAxioms`.

This structure omits the `sdiff`, `hnot` fields, which can be recovered using
`Order.Coframe.ofMinimalAxioms`. -/
class Order.Coframe.MinimalAxioms (α : Type u) extends CompleteLattice α where
  iInf_sup_le_sup_sInf (a : α) (s : Set α) : ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

Minimal Axioms for Coframes

Informal description

The structure `Order.Coframe.MinimalAxioms` provides the minimal axioms required to verify that a complete lattice is a coframe, where finite joins (⊔) distribute over arbitrary meets (⨅). This structure is intended for internal use in constructing instances of `Order.Coframe` via `Order.Coframe.ofMinimalAxioms` and omits certain fields like `sdiff` and `hnot`, which can be recovered in the full coframe definition.

Order.Frame structure

(α : Type*) extends CompleteLattice α, HeytingAlgebra α

Full source

/-- A frame, aka complete Heyting algebra, is a complete lattice whose `⊓` distributes over `⨆`. -/
class Order.Frame (α : Type*) extends CompleteLattice α, HeytingAlgebra α where

Frame (Complete Heyting Algebra)

Informal description

A frame (also known as a complete Heyting algebra) is a complete lattice $\alpha$ equipped with a Heyting algebra structure, where finite meets $\sqcap$ distribute over arbitrary joins $\bigsqcup$. That is, for any element $a \in \alpha$ and any subset $s \subseteq \alpha$, the following holds: \[ a \sqcap \bigsqcup s = \bigsqcup_{b \in s} (a \sqcap b). \]

inf_sSup_eq theorem

{α : Type*} [Order.Frame α] {s : Set α} {a : α} : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b

Full source

/-- `⊓` distributes over `⨆`. -/
theorem inf_sSup_eq {α : Type*} [Order.Frame α] {s : Set α} {a : α} :
    a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b :=
  gc_inf_himp.l_sSup

Meet Distributes Over Supremum in Frames

Informal description

In a frame $\alpha$, for any element $a \in \alpha$ and any subset $s \subseteq \alpha$, the meet of $a$ with the supremum of $s$ equals the supremum of the meets of $a$ with each element of $s$. That is, \[ a \sqcap \left( \bigsqcup_{b \in s} b \right) = \bigsqcup_{b \in s} (a \sqcap b). \]

Order.Coframe structure

(α : Type*) extends CompleteLattice α, CoheytingAlgebra α

Full source

/-- A coframe, aka complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice
whose `⊔` distributes over `⨅`. -/
class Order.Coframe (α : Type*) extends CompleteLattice α, CoheytingAlgebra α where

Coframe (Complete Brouwer Algebra)

Informal description

A coframe, also known as a complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice in which the join operation $\sqcup$ distributes over arbitrary meets $\bigsqcap$. More precisely, for any element $a$ and any subset $s$ of the lattice, the following distributive law holds: \[ a \sqcup \bigsqcap s = \bigsqcap_{b \in s} (a \sqcup b). \] This structure extends both a complete lattice and a co-Heyting algebra.

sup_sInf_eq theorem

{α : Type*} [Order.Coframe α] {s : Set α} {a : α} : a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b

Full source

/-- `⊔` distributes over `⨅`. -/
theorem sup_sInf_eq {α : Type*} [Order.Coframe α] {s : Set α} {a : α} :
    a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b :=
  gc_sdiff_sup.u_sInf

Join Distributes Over Infimum in Coframes

Informal description

In a coframe $\alpha$, for any element $a \in \alpha$ and any subset $s \subseteq \alpha$, the join of $a$ with the infimum of $s$ equals the infimum of the joins of $a$ with each element of $s$. That is, \[ a \sqcup \left( \bigsqcap_{b \in s} b \right) = \bigsqcap_{b \in s} (a \sqcup b). \]

CompleteDistribLattice.MinimalAxioms structure

(α : Type u)
    extends CompleteLattice α,
      toFrameMinimalAxioms : Frame.MinimalAxioms α,
      toCoframeMinimalAxioms : Coframe.MinimalAxioms α

Full source

/-- Structure containing the minimal axioms required to check that an order is a complete
distributive lattice. Do NOT use, except for implementing `CompleteDistribLattice` via
`CompleteDistribLattice.ofMinimalAxioms`.

This structure omits the `himp`, `compl`, `sdiff`, `hnot` fields, which can be recovered using
`CompleteDistribLattice.ofMinimalAxioms`. -/
structure CompleteDistribLattice.MinimalAxioms (α : Type u)
    extends CompleteLattice α,
      toFrameMinimalAxioms : Frame.MinimalAxioms α,
      toCoframeMinimalAxioms : Coframe.MinimalAxioms α where

Minimal Axioms for Complete Distributive Lattice

Informal description

The structure `CompleteDistribLattice.MinimalAxioms` captures the minimal axioms required to verify that an order is a complete distributive lattice. It extends a complete lattice with two additional structures: `Frame.MinimalAxioms` (ensuring finite meets distribute over arbitrary joins) and `Coframe.MinimalAxioms` (ensuring finite joins distribute over arbitrary meets). This structure is intended solely for implementing `CompleteDistribLattice` via `CompleteDistribLattice.ofMinimalAxioms` and should not be used directly.

CompleteDistribLattice structure

(α : Type*) extends Frame α, Coframe α, BiheytingAlgebra α

Full source

/-- A complete distributive lattice is a complete lattice whose `⊔` and `⊓` respectively
distribute over `⨅` and `⨆`. -/
class CompleteDistribLattice (α : Type*) extends Frame α, Coframe α, BiheytingAlgebra α

Complete Distributive Lattice

Informal description

A complete distributive lattice is a complete lattice where finite meets distribute over arbitrary joins and finite joins distribute over arbitrary meets. That is, for any element $a$ and any family of elements $(f_i)_{i \in I}$, the following identities hold: 1. $a \sqcap \left( \bigsqcup_{i \in I} f_i \right) = \bigsqcup_{i \in I} (a \sqcap f_i)$ 2. $a \sqcup \left( \bigsqcap_{i \in I} f_i \right) = \bigsqcap_{i \in I} (a \sqcup f_i)$ Additionally, it is a bi-Heyting algebra, meaning it has both Heyting and co-Heyting algebra structures.

CompletelyDistribLattice.MinimalAxioms structure

(α : Type u) extends CompleteLattice α

Full source

/-- Structure containing the minimal axioms required to check that an order is a completely
distributive. Do NOT use, except for implementing `CompletelyDistribLattice` via
`CompletelyDistribLattice.ofMinimalAxioms`.

This structure omits the `himp`, `compl`, `sdiff`, `hnot` fields, which can be recovered using
`CompletelyDistribLattice.ofMinimalAxioms`. -/
structure CompletelyDistribLattice.MinimalAxioms (α : Type u) extends CompleteLattice α where
  protected iInf_iSup_eq {ι : Type u} {κ : ι → Type u} (f : ∀ a, κ a → α) :
    (⨅ a, ⨆ b, f a b) = ⨆ g : ∀ a, κ a, ⨅ a, f a (g a)

Minimal Axioms for Completely Distributive Lattices

Informal description

The structure `CompletelyDistribLattice.MinimalAxioms` captures the minimal axioms required to verify that a complete lattice is completely distributive. It extends the structure of a complete lattice and serves as a foundation for implementing `CompletelyDistribLattice` through `CompletelyDistribLattice.ofMinimalAxioms`.

CompletelyDistribLattice structure

(α : Type u) extends CompleteLattice α, BiheytingAlgebra α

Full source

/-- A completely distributive lattice is a complete lattice whose `⨅` and `⨆`
distribute over each other. -/
class CompletelyDistribLattice (α : Type u) extends CompleteLattice α, BiheytingAlgebra α where
  protected iInf_iSup_eq {ι : Type u} {κ : ι → Type u} (f : ∀ a, κ a → α) :
    (⨅ a, ⨆ b, f a b) = ⨆ g : ∀ a, κ a, ⨅ a, f a (g a)

Completely Distributive Lattice

Informal description

A completely distributive lattice is a complete lattice $\alpha$ where arbitrary meets $\bigsqcap$ and arbitrary joins $\bigsqcup$ distribute over each other, satisfying the following property: \[ \bigsqcap_{a} \bigsqcup_{b} f(a, b) = \bigsqcup_{g} \bigsqcap_{a} f(a, g(a)) \] for any family of elements $f(a, b)$ in $\alpha$. Additionally, it extends the structure of a bi-Heyting algebra, which provides both Heyting algebra and co-Heyting algebra operations.

le_iInf_iSup theorem

[CompleteLattice α] {f : ∀ a, κ a → α} : (⨆ g : ∀ a, κ a, ⨅ a, f a (g a)) ≤ ⨅ a, ⨆ b, f a b

Full source

theorem le_iInf_iSup [CompleteLattice α] {f : ∀ a, κ a → α} :
    (⨆ g : ∀ a, κ a, ⨅ a, f a (g a)) ≤ ⨅ a, ⨆ b, f a b :=
  iSup_le fun _ => le_iInf fun a => le_trans (iInf_le _ a) (le_iSup _ _)

Supremum-Infimum Inequality in Complete Lattices

Informal description

Let $\alpha$ be a complete lattice and let $f : \prod_{a} \kappa_a \to \alpha$ be a family of elements in $\alpha$. Then the following inequality holds: \[ \bigsqcup_{g : \prod_{a} \kappa_a} \bigsqcap_{a} f_a(g(a)) \leq \bigsqcap_{a} \bigsqcup_{b} f_a(b). \] Here, the supremum is taken over all functions $g$ mapping each index $a$ to an element of $\kappa_a$, and the infimum is taken over all indices $a$.

iSup_iInf_le theorem

[CompleteLattice α] {f : ∀ a, κ a → α} : ⨆ a, ⨅ b, f a b ≤ ⨅ g : ∀ a, κ a, ⨆ a, f a (g a)

Full source

lemma iSup_iInf_le [CompleteLattice α] {f : ∀ a, κ a → α} :
    ⨆ a, ⨅ b, f a b ≤ ⨅ g : ∀ a, κ a, ⨆ a, f a (g a) :=
  le_iInf_iSup (α := αᵒᵈ)

Infimum-Supremum Inequality in Complete Lattices

Informal description

Let $\alpha$ be a complete lattice and let $f : \prod_{a} \kappa_a \to \alpha$ be a family of elements in $\alpha$. Then the following inequality holds: \[ \bigsqcup_{a} \bigsqcap_{b} f(a, b) \leq \bigsqcap_{g : \prod_{a} \kappa_a} \bigsqcup_{a} f(a, g(a)). \] Here, the supremum is taken over all indices $a$, the infimum is taken over all indices $b$ for each $a$, and the infimum on the right is taken over all functions $g$ mapping each index $a$ to an element of $\kappa_a$.

Order.Frame.MinimalAxioms.inf_sSup_eq theorem

: a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b

Full source

lemma inf_sSup_eq : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b :=
  (minAx.inf_sSup_le_iSup_inf _ _).antisymm iSup_inf_le_inf_sSup

Frame Distributivity: Meet Distributes over Supremum

Informal description

Let $\alpha$ be a complete lattice satisfying the minimal frame axioms. For any element $a \in \alpha$ and any subset $s \subseteq \alpha$, the meet of $a$ with the supremum of $s$ equals the supremum of the meets of $a$ with each element $b \in s$: \[ a \sqcap \bigsqcup s = \bigsqcup_{b \in s} (a \sqcap b). \]

Order.Frame.MinimalAxioms.sSup_inf_eq theorem

: sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Full source

lemma sSup_inf_eq : sSupsSup s ⊓ b = ⨆ a ∈ s, a ⊓ b := by
  simpa only [inf_comm] using @inf_sSup_eq α _ s b

Frame Distributivity: Supremum-Meet Identity $\left(\bigsqcup s\right) \sqcap b = \bigsqcup_{a \in s} (a \sqcap b)$

Informal description

Let $\alpha$ be a complete lattice satisfying the minimal frame axioms. For any subset $s \subseteq \alpha$ and any element $b \in \alpha$, the meet of the supremum of $s$ with $b$ equals the supremum of the meets of each element $a \in s$ with $b$: \[ \left(\bigsqcup s\right) \sqcap b = \bigsqcup_{a \in s} (a \sqcap b). \]

Order.Frame.MinimalAxioms.iSup_inf_eq theorem

(f : ι → α) (a : α) : (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Full source

lemma iSup_inf_eq (f : ι → α) (a : α) : (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a := by
  rw [iSup, sSup_inf_eq, iSup_range]

Frame Distributivity: $\left(\bigsqcup_i f_i\right) \sqcap a = \bigsqcup_i (f_i \sqcap a)$

Informal description

Let $\alpha$ be a complete lattice satisfying the minimal frame axioms. For any indexed family of elements $f : \iota \to \alpha$ and any element $a \in \alpha$, the meet of the supremum of $f$ with $a$ equals the supremum of the meets of each $f_i$ with $a$: \[ \left(\bigsqcup_{i} f_i\right) \sqcap a = \bigsqcup_{i} (f_i \sqcap a). \]

Order.Frame.MinimalAxioms.inf_iSup_eq theorem

(a : α) (f : ι → α) : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i

Full source

lemma inf_iSup_eq (a : α) (f : ι → α) : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i := by
  simpa only [inf_comm] using minAx.iSup_inf_eq f a

Frame Distributivity: $a \sqcap \left( \bigsqcup_i f_i \right) = \bigsqcup_i (a \sqcap f_i)$

Informal description

Let $\alpha$ be a complete lattice satisfying the minimal frame axioms. For any element $a \in \alpha$ and any indexed family of elements $f : \iota \to \alpha$, the meet of $a$ with the supremum of $f$ equals the supremum of the meets of $a$ with each $f_i$: \[ a \sqcap \left( \bigsqcup_{i} f_i \right) = \bigsqcup_{i} (a \sqcap f_i). \]

Order.Frame.MinimalAxioms.inf_iSup₂_eq theorem

{f : ∀ i, κ i → α} (a : α) : (a ⊓ ⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, a ⊓ f i j

Full source

lemma inf_iSup₂_eq {f : ∀ i, κ i → α} (a : α) : (a ⊓ ⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, a ⊓ f i j := by
  simp only [inf_iSup_eq]

Frame Distributivity for Doubly Indexed Joins: $a \sqcap \left( \bigsqcup_{i,j} f_{i,j} \right) = \bigsqcup_{i,j} (a \sqcap f_{i,j})$

Informal description

Let $\alpha$ be a complete lattice satisfying the minimal frame axioms. For any element $a \in \alpha$ and any doubly indexed family of elements $f : \forall i, \kappa_i \to \alpha$, the meet of $a$ with the supremum of the suprema of $f$ equals the supremum of the suprema of the meets of $a$ with each $f_{i,j}$: \[ a \sqcap \left( \bigsqcup_{i} \bigsqcup_{j} f_{i,j} \right) = \bigsqcup_{i} \bigsqcup_{j} (a \sqcap f_{i,j}). \]

Order.Frame.MinimalAxioms.of definition

[Frame α] : MinimalAxioms α

Full source

/-- The `Order.Frame.MinimalAxioms` element corresponding to a frame. -/
def of [Frame α] : MinimalAxioms α where
  __ :=  ‹Frame α›
  inf_sSup_le_iSup_inf a s := _root_.inf_sSup_eq.le

Minimal Frame Axioms Construction from Frame

Informal description

Given a frame $\alpha$, the structure `Order.Frame.MinimalAxioms` is constructed by inheriting the complete lattice structure from $\alpha$ and verifying that finite meets distribute over arbitrary joins, i.e., for any element $a \in \alpha$ and any family of elements $(f_i)_{i \in \iota}$ in $\alpha$, the following holds: \[ a \sqcap \left( \bigsqcup_{i} f_i \right) = \bigsqcup_{i} (a \sqcap f_i). \] This structure serves as an intermediate step in constructing a full frame structure, ensuring that the minimal axioms required for a frame are satisfied.

Order.Frame.ofMinimalAxioms abbrev

(minAx : MinimalAxioms α) : Frame α

Full source

/-- Construct a frame instance using the minimal amount of work needed.

This sets `a ⇨ b := sSup {c | c ⊓ a ≤ b}` and `aᶜ := a ⇨ ⊥`. -/
-- See note [reducible non instances]
abbrev ofMinimalAxioms (minAx : MinimalAxioms α) : Frame α where
  __ := minAx
  compl a := sSup {c | c ⊓ a ≤ ⊥}
  himp a b := sSup {c | c ⊓ a ≤ b}
  le_himp_iff _ b c :=
    ⟨fun h ↦ (inf_le_inf_right _ h).trans (by simp [minAx.sSup_inf_eq]), fun h ↦ le_sSup h⟩
  himp_bot _ := rfl

Frame Construction from Minimal Axioms

Informal description

Given a complete lattice $\alpha$ satisfying the minimal frame axioms (i.e., finite meets distribute over arbitrary joins), the structure `Order.Frame.ofMinimalAxioms` constructs a frame instance on $\alpha$ by defining the Heyting implication $a \to b$ as the supremum $\bigsqcup \{c \mid c \sqcap a \leq b\}$ and the complement $a^\complement$ as $a \to \bot$.

Order.Coframe.MinimalAxioms.sup_sInf_eq theorem

: a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b

Full source

lemma sup_sInf_eq : a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b :=
  sup_sInf_le_iInf_sup.antisymm (minAx.iInf_sup_le_sup_sInf _ _)

Join-Infimum Distributivity in Coframes

Informal description

In a coframe $\alpha$, for any element $a \in \alpha$ and any subset $s \subseteq \alpha$, the join of $a$ with the infimum of $s$ equals the infimum of the joins of $a$ with each element $b \in s$. That is, $$ a \sqcup \bigsqcap s = \bigsqcap_{b \in s} (a \sqcup b). $$

Order.Coframe.MinimalAxioms.sInf_sup_eq theorem

: sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b

Full source

lemma sInf_sup_eq : sInfsInf s ⊔ b = ⨅ a ∈ s, a ⊔ b := by
  simpa only [sup_comm] using @sup_sInf_eq α _ s b

Infimum-Join Distributivity in Coframes

Informal description

In a coframe $\alpha$, for any subset $s \subseteq \alpha$ and any element $b \in \alpha$, the join of the infimum of $s$ with $b$ equals the infimum of the joins of each element $a \in s$ with $b$. That is, $$ \bigsqcap s \sqcup b = \bigsqcap_{a \in s} (a \sqcup b). $$

Order.Coframe.MinimalAxioms.iInf_sup_eq theorem

(f : ι → α) (a : α) : (⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a

Full source

lemma iInf_sup_eq (f : ι → α) (a : α) : (⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a := by
  rw [iInf, sInf_sup_eq, iInf_range]

Infimum-Join Distributivity for Indexed Families in Coframes

Informal description

In a coframe $\alpha$, for any indexed family of elements $f : \iota \to \alpha$ and any element $a \in \alpha$, the join of the infimum of the family with $a$ equals the infimum of the joins of each element $f_i$ with $a$. That is, $$ \left(\bigsqcap_{i} f_i\right) \sqcup a = \bigsqcap_{i} (f_i \sqcup a). $$

Order.Coframe.MinimalAxioms.sup_iInf_eq theorem

(a : α) (f : ι → α) : (a ⊔ ⨅ i, f i) = ⨅ i, a ⊔ f i

Full source

lemma sup_iInf_eq (a : α) (f : ι → α) : (a ⊔ ⨅ i, f i) = ⨅ i, a ⊔ f i := by
  simpa only [sup_comm] using minAx.iInf_sup_eq f a

Join-Infimum Distributivity in Coframes

Informal description

In a coframe $\alpha$, for any element $a \in \alpha$ and any indexed family of elements $f : \iota \to \alpha$, the join of $a$ with the infimum of the family equals the infimum of the joins of $a$ with each element $f_i$. That is, $$ a \sqcup \left(\bigsqcap_{i} f_i\right) = \bigsqcap_{i} (a \sqcup f_i). $$

Order.Coframe.MinimalAxioms.sup_iInf₂_eq theorem

{f : ∀ i, κ i → α} (a : α) : (a ⊔ ⨅ i, ⨅ j, f i j) = ⨅ i, ⨅ j, a ⊔ f i j

Full source

lemma sup_iInf₂_eq {f : ∀ i, κ i → α} (a : α) : (a ⊔ ⨅ i, ⨅ j, f i j) = ⨅ i, ⨅ j, a ⊔ f i j := by
  simp only [sup_iInf_eq]

Doubly Indexed Join-Infimum Distributivity in Coframes

Informal description

In a coframe $\alpha$, for any element $a \in \alpha$ and any doubly indexed family of elements $f : \forall i, \kappa_i \to \alpha$, the join of $a$ with the infimum of the doubly indexed family equals the infimum of the joins of $a$ with each element $f_{i,j}$. That is, $$ a \sqcup \left(\bigsqcap_{i} \bigsqcap_{j} f_{i,j}\right) = \bigsqcap_{i} \bigsqcap_{j} (a \sqcup f_{i,j}). $$

Order.Coframe.MinimalAxioms.of definition

[Coframe α] : MinimalAxioms α

Full source

/-- The `Order.Coframe.MinimalAxioms` element corresponding to a frame. -/
def of [Coframe α] : MinimalAxioms α where
  __ := ‹Coframe α›
  iInf_sup_le_sup_sInf a s := _root_.sup_sInf_eq.ge

Minimal Axioms for Coframes

Informal description

Given a coframe $\alpha$, the structure `Order.Coframe.MinimalAxioms.of` provides the minimal axioms required to verify that $\alpha$ is a coframe, where finite joins (⊔) distribute over arbitrary meets (⨅). Specifically, it ensures that for any element $a$ and any subset $s$ of the lattice, the following distributive law holds: \[ a \sqcup \bigsqcap s = \bigsqcap_{b \in s} (a \sqcup b). \]

Order.Coframe.ofMinimalAxioms abbrev

(minAx : MinimalAxioms α) : Coframe α

Full source

/-- Construct a coframe instance using the minimal amount of work needed.

This sets `a \ b := sInf {c | a ≤ b ⊔ c}` and `￢a := ⊤ \ a`. -/
-- See note [reducible non instances]
abbrev ofMinimalAxioms (minAx : MinimalAxioms α) : Coframe α where
  __ := minAx
  hnot a := sInf {c | ⊤ ≤ a ⊔ c}
  sdiff a b := sInf {c | a ≤ b ⊔ c}
  sdiff_le_iff a b _ :=
    ⟨fun h ↦ (sup_le_sup_left h _).trans' (by simp [minAx.sup_sInf_eq]), fun h ↦ sInf_le h⟩
  top_sdiff _ := rfl

Coframe Construction from Minimal Axioms

Informal description

Given a complete lattice $\alpha$ equipped with minimal axioms for a coframe (where finite joins distribute over arbitrary meets), the function `Order.Coframe.ofMinimalAxioms` constructs a coframe structure on $\alpha$. Specifically, it defines the relative pseudocomplement (Heyting implication) $a \setminus b$ as the infimum of the set $\{c \mid a \leq b \sqcup c\}$ and the pseudocomplement $\neg a$ as $\top \setminus a$.

CompleteDistribLattice.MinimalAxioms.of definition

[CompleteDistribLattice α] : MinimalAxioms α

Full source

/-- The `CompleteDistribLattice.MinimalAxioms` element corresponding to a complete distrib lattice.
-/
def of [CompleteDistribLattice α] : MinimalAxioms α where
  __ := ‹CompleteDistribLattice α›
  inf_sSup_le_iSup_inf a s:= inf_sSup_eq.le
  iInf_sup_le_sup_sInf a s:= sup_sInf_eq.ge

Minimal Axioms for Complete Distributive Lattice

Informal description

Given a complete distributive lattice $\alpha$, the structure `CompleteDistribLattice.MinimalAxioms.of` provides the minimal axioms required to verify that $\alpha$ is a complete distributive lattice. Specifically, it ensures that finite meets distribute over arbitrary joins and finite joins distribute over arbitrary meets, i.e., for any element $a$ and any family of elements $(f_i)_{i \in I}$, the following identities hold: 1. $a \sqcap \left( \bigsqcup_{i \in I} f_i \right) = \bigsqcup_{i \in I} (a \sqcap f_i)$ 2. $a \sqcup \left( \bigsqcap_{i \in I} f_i \right) = \bigsqcap_{i \in I} (a \sqcup f_i)$

CompleteDistribLattice.MinimalAxioms.toFrame abbrev

: Frame.MinimalAxioms α

Full source

/-- Turn minimal axioms for `CompleteDistribLattice` into minimal axioms for `Order.Frame`. -/
abbrev toFrame : Frame.MinimalAxioms α := minAx.toFrameMinimalAxioms

Frame Axioms from Complete Distributive Lattice Minimal Axioms

Informal description

Given a complete distributive lattice $\alpha$ with minimal axioms, the structure `CompleteDistribLattice.MinimalAxioms.toFrame` provides the minimal axioms required to verify that $\alpha$ is a frame, where finite meets ($\sqcap$) distribute over arbitrary joins ($\bigsqcup$).

CompleteDistribLattice.MinimalAxioms.toCoframe abbrev

: Coframe.MinimalAxioms α

Full source

/-- Turn minimal axioms for `CompleteDistribLattice` into minimal axioms for `Order.Coframe`. -/
abbrev toCoframe : Coframe.MinimalAxioms α where __ := minAx

Minimal Axioms for Coframe from Complete Distributive Lattice

Informal description

Given a complete distributive lattice $\alpha$ with minimal axioms, the structure `CompleteDistribLattice.MinimalAxioms.toCoframe` provides the minimal axioms required to verify that $\alpha$ is a coframe, where finite joins ($\sqcup$) distribute over arbitrary meets ($\bigsqcap$).

CompleteDistribLattice.ofMinimalAxioms abbrev

(minAx : MinimalAxioms α) : CompleteDistribLattice α

Full source

/-- Construct a complete distrib lattice instance using the minimal amount of work needed.

This sets `a ⇨ b := sSup {c | c ⊓ a ≤ b}`, `aᶜ := a ⇨ ⊥`, `a \ b := sInf {c | a ≤ b ⊔ c}` and
`￢a := ⊤ \ a`. -/
-- See note [reducible non instances]
abbrev ofMinimalAxioms (minAx : MinimalAxioms α) : CompleteDistribLattice α where
  __ := Frame.ofMinimalAxioms minAx.toFrame
  __ := Coframe.ofMinimalAxioms minAx.toCoframe

Construction of Complete Distributive Lattice from Minimal Axioms

Informal description

Given a complete lattice $\alpha$ equipped with minimal axioms for a complete distributive lattice (where finite meets distribute over arbitrary joins and finite joins distribute over arbitrary meets), the function `CompleteDistribLattice.ofMinimalAxioms` constructs a complete distributive lattice structure on $\alpha$. Specifically, it defines: 1. The Heyting implication $a \to b$ as $\bigsqcup \{c \mid c \sqcap a \leq b\}$, 2. The complement $a^\complement$ as $a \to \bot$, 3. The relative pseudocomplement $a \setminus b$ as $\bigsqcap \{c \mid a \leq b \sqcup c\}$, 4. The pseudocomplement $\neg a$ as $\top \setminus a$.

CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq' theorem

 (f : ∀ a, κ a → α) :
  let _ := minAx.toCompleteLattice
  ⨅ i, ⨆ j, f i j = ⨆ g : ∀ i, κ i, ⨅ i, f i (g i)

Full source

lemma iInf_iSup_eq' (f : ∀ a, κ a → α) :
    let _ := minAx.toCompleteLattice
    ⨅ i, ⨆ j, f i j = ⨆ g : ∀ i, κ i, ⨅ i, f i (g i) := by
  let _ := minAx.toCompleteLattice
  refine le_antisymm ?_ le_iInf_iSup
  calc
    _ = ⨅ a : range (range <| f ·), ⨆ b : a.1, b.1 := by
      simp_rw [iInf_subtype, iInf_range, iSup_subtype, iSup_range]
    _ = _ := minAx.iInf_iSup_eq _
    _ ≤ _ := iSup_le fun g => by
      refine le_trans ?_ <| le_iSup _ fun a => Classical.choose (g ⟨_, a, rfl⟩).2
      refine le_iInf fun a => le_trans (iInf_le _ ⟨range (f a), a, rfl⟩) ?_
      rw [← Classical.choose_spec (g ⟨_, a, rfl⟩).2]

Complete Distributivity: $\bigsqcap_i \bigsqcup_j f_{ij} = \bigsqcup_g \bigsqcap_i f_{i(g(i))}$

Informal description

Let $\alpha$ be a complete lattice satisfying the minimal axioms for complete distributivity. For any family of elements $f : \prod_{i} \kappa_i \to \alpha$, the following equality holds: \[ \bigsqcap_{i} \bigsqcup_{j} f_i(j) = \bigsqcup_{g : \prod_{i} \kappa_i} \bigsqcap_{i} f_i(g(i)). \] Here, the infimum is taken over all indices $i$, the supremum inside is taken over all $j \in \kappa_i$, and the outer supremum is taken over all functions $g$ mapping each index $i$ to an element of $\kappa_i$.

CompletelyDistribLattice.MinimalAxioms.iSup_iInf_eq theorem

 (f : ∀ i, κ i → α) :
  let _ := minAx.toCompleteLattice
  ⨆ i, ⨅ j, f i j = ⨅ g : ∀ i, κ i, ⨆ i, f i (g i)

Full source

lemma iSup_iInf_eq (f : ∀ i, κ i → α) :
    let _ := minAx.toCompleteLattice
    ⨆ i, ⨅ j, f i j = ⨅ g : ∀ i, κ i, ⨆ i, f i (g i) := by
  let _ := minAx.toCompleteLattice
  refine le_antisymm iSup_iInf_le ?_
  rw [minAx.iInf_iSup_eq']
  refine iSup_le fun g => ?_
  have ⟨a, ha⟩ : ∃ a, ∀ b, ∃ f, ∃ h : a = g f, h ▸ b = f (g f) := of_not_not fun h => by
    push_neg at h
    choose h hh using h
    have := hh _ h rfl
    contradiction
  refine le_trans ?_ (le_iSup _ a)
  refine le_iInf fun b => ?_
  obtain ⟨h, rfl, rfl⟩ := ha b
  exact iInf_le _ _

Complete Distributivity: $\bigsqcup_i \bigsqcap_j f_{ij} = \bigsqcap_g \bigsqcup_i f_{i(g(i))}$

Informal description

Let $\alpha$ be a complete lattice satisfying the minimal axioms for complete distributivity. For any family of elements $f : \prod_{i} \kappa_i \to \alpha$, the following equality holds: \[ \bigsqcup_{i} \bigsqcap_{j} f_i(j) = \bigsqcap_{g : \prod_{i} \kappa_i} \bigsqcup_{i} f_i(g(i)). \] Here, the supremum is taken over all indices $i$, the infimum inside is taken over all $j \in \kappa_i$, and the outer infimum is taken over all functions $g$ mapping each index $i$ to an element of $\kappa_i$.

CompletelyDistribLattice.MinimalAxioms.toCompleteDistribLattice abbrev

: CompleteDistribLattice.MinimalAxioms α

Full source

/-- Turn minimal axioms for `CompletelyDistribLattice` into minimal axioms for
`CompleteDistribLattice`. -/
abbrev toCompleteDistribLattice : CompleteDistribLattice.MinimalAxioms α where
  __ := minAx
  inf_sSup_le_iSup_inf a s := by
    let _ := minAx.toCompleteLattice
    calc
      _ = ⨅ i : ULift.{u} Bool, ⨆ j : match i with | .up true => PUnit.{u + 1} | .up false => s,
          match i with
          | .up true => a
          | .up false => j := by simp [sSup_eq_iSup', iSup_unique, iInf_bool_eq]
      _ ≤ _ := by
        simp only [minAx.iInf_iSup_eq, iInf_ulift, iInf_bool_eq, iSup_le_iff]
        exact fun x ↦ le_biSup _ (x (.up false)).2
  iInf_sup_le_sup_sInf a s := by
    let _ := minAx.toCompleteLattice
    calc
      _ ≤ ⨆ i : ULift.{u} Bool, ⨅ j : match i with | .up true => PUnit.{u + 1} | .up false => s,
          match i with
          | .up true => a
          | .up false => j := by
        simp only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]
        exact fun x ↦ biInf_le _ (x (.up false)).2
      _ = _ := by simp [sInf_eq_iInf', iInf_unique, iSup_bool_eq]

Implication from Completely Distributive to Complete Distributive Lattice Axioms

Informal description

The structure `CompletelyDistribLattice.MinimalAxioms` implies the structure `CompleteDistribLattice.MinimalAxioms` for a type `α`. That is, any completely distributive lattice satisfies the minimal axioms of a complete distributive lattice.

CompletelyDistribLattice.MinimalAxioms.of definition

[CompletelyDistribLattice α] : MinimalAxioms α

Full source

/-- The `CompletelyDistribLattice.MinimalAxioms` element corresponding to a frame. -/
def of [CompletelyDistribLattice α] : MinimalAxioms α := { ‹CompletelyDistribLattice α› with }

Minimal Axioms for Completely Distributive Lattices from Completely Distributive Lattice

Informal description

Given a completely distributive lattice $\alpha$, the structure `CompletelyDistribLattice.MinimalAxioms.of` provides the minimal axioms required to verify that $\alpha$ is completely distributive. This structure extends the complete lattice structure of $\alpha$ and serves as a foundation for implementing completely distributive lattices through `CompletelyDistribLattice.ofMinimalAxioms`.

CompletelyDistribLattice.ofMinimalAxioms abbrev

(minAx : MinimalAxioms α) : CompletelyDistribLattice α

Full source

/-- Construct a completely distributive lattice instance using the minimal amount of work needed.

This sets `a ⇨ b := sSup {c | c ⊓ a ≤ b}`, `aᶜ := a ⇨ ⊥`, `a \ b := sInf {c | a ≤ b ⊔ c}` and
`￢a := ⊤ \ a`. -/
-- See note [reducible non instances]
abbrev ofMinimalAxioms (minAx : MinimalAxioms α) : CompletelyDistribLattice α where
  __ := minAx
  __ := CompleteDistribLattice.ofMinimalAxioms minAx.toCompleteDistribLattice

Construction of Completely Distributive Lattice from Minimal Axioms

Informal description

Given a complete lattice $\alpha$ equipped with minimal axioms for a completely distributive lattice, the function `CompletelyDistribLattice.ofMinimalAxioms` constructs a completely distributive lattice structure on $\alpha$. Specifically, it defines: 1. The Heyting implication $a \to b$ as $\bigsqcup \{c \mid c \sqcap a \leq b\}$, 2. The complement $a^\complement$ as $a \to \bot$, 3. The relative pseudocomplement $a \setminus b$ as $\bigsqcap \{c \mid a \leq b \sqcup c\}$, 4. The pseudocomplement $\neg a$ as $\top \setminus a$.

iInf_iSup_eq theorem

[CompletelyDistribLattice α] {f : ∀ a, κ a → α} : (⨅ a, ⨆ b, f a b) = ⨆ g : ∀ a, κ a, ⨅ a, f a (g a)

Full source

theorem iInf_iSup_eq [CompletelyDistribLattice α] {f : ∀ a, κ a → α} :
    (⨅ a, ⨆ b, f a b) = ⨆ g : ∀ a, κ a, ⨅ a, f a (g a) :=
  CompletelyDistribLattice.MinimalAxioms.of.iInf_iSup_eq' _

Complete Distributivity: $\bigsqcap_a \bigsqcup_b f(a, b) = \bigsqcup_g \bigsqcap_a f(a, g(a))$

Informal description

Let $\alpha$ be a completely distributive lattice. For any family of elements $f : \prod_{a} \kappa_a \to \alpha$, the following equality holds: \[ \bigsqcap_{a} \bigsqcup_{b} f(a, b) = \bigsqcup_{g : \prod_{a} \kappa_a} \bigsqcap_{a} f(a, g(a)). \] Here, the left-hand side is the infimum over $a$ of the supremum over $b$ of $f(a, b)$, and the right-hand side is the supremum over all functions $g$ (mapping each $a$ to an element of $\kappa_a$) of the infimum over $a$ of $f(a, g(a))$.

iSup_iInf_eq theorem

[CompletelyDistribLattice α] {f : ∀ a, κ a → α} : (⨆ a, ⨅ b, f a b) = ⨅ g : ∀ a, κ a, ⨆ a, f a (g a)

Full source

theorem iSup_iInf_eq [CompletelyDistribLattice α] {f : ∀ a, κ a → α} :
    (⨆ a, ⨅ b, f a b) = ⨅ g : ∀ a, κ a, ⨆ a, f a (g a) :=
  CompletelyDistribLattice.MinimalAxioms.of.iSup_iInf_eq _

Complete Distributivity: $\bigsqcup_a \bigsqcap_b f(a, b) = \bigsqcap_g \bigsqcup_a f(a, g(a))$

Informal description

Let $\alpha$ be a completely distributive lattice. For any family of elements $f : \prod_{a} \kappa_a \to \alpha$, the following equality holds: \[ \bigsqcup_{a} \bigsqcap_{b} f(a, b) = \bigsqcap_{g : \prod_{a} \kappa_a} \bigsqcup_{a} f(a, g(a)). \] Here, the left-hand side is the supremum over $a$ of the infimum over $b$ of $f(a, b)$, and the right-hand side is the infimum over all functions $g$ (mapping each $a$ to an element of $\kappa_a$) of the supremum over $a$ of $f(a, g(a))$.

CompletelyDistribLattice.toCompleteDistribLattice instance

[CompletelyDistribLattice α] : CompleteDistribLattice α

Full source

instance (priority := 100) CompletelyDistribLattice.toCompleteDistribLattice
    [CompletelyDistribLattice α] : CompleteDistribLattice α where
  __ := ‹CompletelyDistribLattice α›

Completely Distributive Lattices are Complete Distributive Lattices

Informal description

Every completely distributive lattice $\alpha$ is also a complete distributive lattice.

CompleteLinearOrder.toCompletelyDistribLattice instance

[CompleteLinearOrder α] : CompletelyDistribLattice α

Full source

instance (priority := 100) CompleteLinearOrder.toCompletelyDistribLattice [CompleteLinearOrder α] :
    CompletelyDistribLattice α where
  __ := ‹CompleteLinearOrder α›
  iInf_iSup_eq {α β} g := by
    let lhs := ⨅ a, ⨆ b, g a b
    let rhs := ⨆ h : ∀ a, β a, ⨅ a, g a (h a)
    suffices lhs ≤ rhs from le_antisymm this le_iInf_iSup
    if h : ∃ x, rhs < x ∧ x < lhs then
      rcases h with ⟨x, hr, hl⟩
      suffices rhs ≥ x from nomatch not_lt.2 this hr
      have : ∀ a, ∃ b, x < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_not_le fun h =>
            lt_irrefl x (lt_of_lt_of_le hl (le_trans (iInf_le _ a) h))
      choose f hf using this
      refine le_trans ?_ (le_iSup _ f)
      exact le_iInf fun a => le_of_lt (hf a)
    else
      refine le_of_not_lt fun hrl : rhs < lhs => not_le_of_lt hrl ?_
      replace h : ∀ x, x ≤ rhs ∨ lhs ≤ x := by
        simpa only [not_exists, not_and_or, not_or, not_lt] using h
      have : ∀ a, ∃ b, rhs < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_lt_of_le hrl (iInf_le _ a)
      choose f hf using this
      have : ∀ a, lhs ≤ g a (f a) := fun a =>
        (h (g a (f a))).resolve_left (by simpa using hf a)
      refine le_trans ?_ (le_iSup _ f)
      exact le_iInf fun a => this _

Complete Linear Orders are Completely Distributive Lattices

Informal description

Every complete linear order $\alpha$ is a completely distributive lattice.

OrderDual.instCoframe instance

: Coframe αᵒᵈ

Full source

instance OrderDual.instCoframe : Coframe αᵒᵈ where
  __ := instCompleteLattice
  __ := instCoheytingAlgebra

Order Dual of a Frame is a Coframe

Informal description

The order dual $\alpha^{\text{op}}$ of any frame $\alpha$ forms a coframe. That is, if $\alpha$ is a complete lattice where finite meets distribute over arbitrary joins, then $\alpha^{\text{op}}$ is a complete lattice where finite joins distribute over arbitrary meets.

sSup_inf_eq theorem

: sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Full source

theorem sSup_inf_eq : sSupsSup s ⊓ b = ⨆ a ∈ s, a ⊓ b := by
  simpa only [inf_comm] using @inf_sSup_eq α _ s b

Supremum-Meet Distributivity in Frames

Informal description

In a frame $\alpha$, for any subset $s \subseteq \alpha$ and any element $b \in \alpha$, the meet of the supremum of $s$ with $b$ equals the supremum of the meets of each element of $s$ with $b$. That is, \[ \left( \bigsqcup s \right) \sqcap b = \bigsqcup_{a \in s} (a \sqcap b). \]

iSup_inf_eq theorem

(f : ι → α) (a : α) : (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Full source

theorem iSup_inf_eq (f : ι → α) (a : α) : (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a := by
  rw [iSup, sSup_inf_eq, iSup_range]

Distributivity of Meet over Indexed Supremum in Frames

Informal description

In a frame $\alpha$, for any indexed family of elements $f : \iota \to \alpha$ and any element $a \in \alpha$, the meet of the supremum of $f$ with $a$ equals the supremum of the meets of each $f_i$ with $a$. That is, \[ \left( \bigsqcup_{i} f_i \right) \sqcap a = \bigsqcup_{i} (f_i \sqcap a). \]

inf_iSup_eq theorem

(a : α) (f : ι → α) : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i

Full source

theorem inf_iSup_eq (a : α) (f : ι → α) : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i := by
  simpa only [inf_comm] using iSup_inf_eq f a

Finite Meet Distributes over Infinite Join in Frames

Informal description

In a frame $\alpha$, for any element $a \in \alpha$ and any indexed family of elements $f : \iota \to \alpha$, the meet of $a$ with the supremum of $f$ equals the supremum of the meets of $a$ with each $f_i$. That is, \[ a \sqcap \left( \bigsqcup_{i} f_i \right) = \bigsqcup_{i} (a \sqcap f_i). \]

iSup₂_inf_eq theorem

{f : ∀ i, κ i → α} (a : α) : (⨆ (i) (j), f i j) ⊓ a = ⨆ (i) (j), f i j ⊓ a

Full source

theorem iSup₂_inf_eq {f : ∀ i, κ i → α} (a : α) :
    (⨆ (i) (j), f i j) ⊓ a = ⨆ (i) (j), f i j ⊓ a := by
  simp only [iSup_inf_eq]

Distributivity of Meet over Doubly Indexed Supremum in Frames

Informal description

Let $\alpha$ be a frame and let $f : \forall i, \kappa_i \to \alpha$ be a doubly indexed family of elements in $\alpha$. For any element $a \in \alpha$, the meet of the supremum of $f$ with $a$ equals the supremum of the meets of each $f_{i,j}$ with $a$. That is, \[ \left( \bigsqcup_{i,j} f_{i,j} \right) \sqcap a = \bigsqcup_{i,j} (f_{i,j} \sqcap a). \]

inf_iSup₂_eq theorem

{f : ∀ i, κ i → α} (a : α) : (a ⊓ ⨆ (i) (j), f i j) = ⨆ (i) (j), a ⊓ f i j

Full source

theorem inf_iSup₂_eq {f : ∀ i, κ i → α} (a : α) :
    (a ⊓ ⨆ (i) (j), f i j) = ⨆ (i) (j), a ⊓ f i j := by
  simp only [inf_iSup_eq]

Distributivity of Meet over Doubly Indexed Supremum in Frames

Informal description

In a frame $\alpha$, for any element $a \in \alpha$ and any doubly indexed family of elements $f : \forall i, \kappa_i \to \alpha$, the meet of $a$ with the supremum of $f$ equals the supremum of the meets of $a$ with each $f_{i,j}$. That is, \[ a \sqcap \left( \bigsqcup_{i,j} f_{i,j} \right) = \bigsqcup_{i,j} (a \sqcap f_{i,j}). \]

iSup_inf_iSup theorem

{ι ι' : Type*} {f : ι → α} {g : ι' → α} : ((⨆ i, f i) ⊓ ⨆ j, g j) = ⨆ i : ι × ι', f i.1 ⊓ g i.2

Full source

theorem iSup_inf_iSup {ι ι' : Type*} {f : ι → α} {g : ι' → α} :
    ((⨆ i, f i) ⊓ ⨆ j, g j) = ⨆ i : ι × ι', f i.1 ⊓ g i.2 := by
  simp_rw [iSup_inf_eq, inf_iSup_eq, iSup_prod]

Distributivity of Meet over Suprema in Frames: $\left( \bigsqcup_i f_i \right) \sqcap \left( \bigsqcup_j g_j \right) = \bigsqcup_{i,j} (f_i \sqcap g_j)$

Informal description

Let $\alpha$ be a frame, and let $f : \iota \to \alpha$ and $g : \iota' \to \alpha$ be two indexed families of elements in $\alpha$. Then the meet of their suprema equals the supremum of the pairwise meets over the product index type. That is, \[ \left( \bigsqcup_{i} f_i \right) \sqcap \left( \bigsqcup_{j} g_j \right) = \bigsqcup_{(i,j) \in \iota \times \iota'} (f_i \sqcap g_j). \]

biSup_inf_biSup theorem

 {ι ι' : Type*} {f : ι → α} {g : ι' → α} {s : Set ι} {t : Set ι'} :
  ((⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j) = ⨆ p ∈ s ×ˢ t, f (p : ι × ι').1 ⊓ g p.2

Full source

theorem biSup_inf_biSup {ι ι' : Type*} {f : ι → α} {g : ι' → α} {s : Set ι} {t : Set ι'} :
    ((⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j) = ⨆ p ∈ s ×ˢ t, f (p : ι × ι').1 ⊓ g p.2 := by
  simp only [iSup_subtype', iSup_inf_iSup]
  exact (Equiv.surjective _).iSup_congr (Equiv.Set.prod s t).symm fun x => rfl

Distributivity of Meet over Bounded Suprema in Frames: $\left( \bigsqcup_{i \in s} f_i \right) \sqcap \left( \bigsqcup_{j \in t} g_j \right) = \bigsqcup_{(i,j) \in s \times t} (f_i \sqcap g_j)$

Informal description

Let $\alpha$ be a frame, and let $f : \iota \to \alpha$ and $g : \iota' \to \alpha$ be two indexed families of elements in $\alpha$, with $s \subseteq \iota$ and $t \subseteq \iota'$ subsets of their respective index sets. Then the meet of the bounded suprema of $f$ over $s$ and $g$ over $t$ equals the supremum of the pairwise meets over the product set $s \times t$. That is, \[ \left( \bigsqcup_{i \in s} f_i \right) \sqcap \left( \bigsqcup_{j \in t} g_j \right) = \bigsqcup_{(i,j) \in s \times t} (f_i \sqcap g_j). \]

sSup_inf_sSup theorem

: sSup s ⊓ sSup t = ⨆ p ∈ s ×ˢ t, (p : α × α).1 ⊓ p.2

Full source

theorem sSup_inf_sSup : sSupsSup s ⊓ sSup t = ⨆ p ∈ s ×ˢ t, (p : α × α).1 ⊓ p.2 := by
  simp only [sSup_eq_iSup, biSup_inf_biSup]

Distributivity of Meet over Suprema in Frames: $\left( \bigsqcup_{a \in s} a \right) \sqcap \left( \bigsqcup_{b \in t} b \right) = \bigsqcup_{(a,b) \in s \times t} (a \sqcap b)$

Informal description

Let $\alpha$ be a frame, and let $s, t \subseteq \alpha$ be subsets of $\alpha$. Then the meet of their suprema equals the supremum of the pairwise meets over the product set $s \times t$. That is, \[ \left( \bigsqcup_{a \in s} a \right) \sqcap \left( \bigsqcup_{b \in t} b \right) = \bigsqcup_{(a,b) \in s \times t} (a \sqcap b). \]

iSup_disjoint_iff theorem

{f : ι → α} : Disjoint (⨆ i, f i) a ↔ ∀ i, Disjoint (f i) a

Full source

theorem iSup_disjoint_iff {f : ι → α} : DisjointDisjoint (⨆ i, f i) a ↔ ∀ i, Disjoint (f i) a := by
  simp only [disjoint_iff, iSup_inf_eq, iSup_eq_bot]

Disjointness of Indexed Supremum: $\bigsqcup_i f_i \perp a \leftrightarrow \forall i, f_i \perp a$

Informal description

For any indexed family of elements $f : \iota \to \alpha$ in a frame $\alpha$ and any element $a \in \alpha$, the supremum $\bigsqcup_i f_i$ is disjoint from $a$ if and only if $f_i$ is disjoint from $a$ for every $i \in \iota$. In symbols: \[ \left( \bigsqcup_i f_i \right) \perp a \leftrightarrow \forall i, f_i \perp a. \]

disjoint_iSup_iff theorem

{f : ι → α} : Disjoint a (⨆ i, f i) ↔ ∀ i, Disjoint a (f i)

Full source

theorem disjoint_iSup_iff {f : ι → α} : DisjointDisjoint a (⨆ i, f i) ↔ ∀ i, Disjoint a (f i) := by
  simpa only [disjoint_comm] using @iSup_disjoint_iff

Disjointness with Indexed Supremum in a Frame

Informal description

For any element $a$ in a frame $\alpha$ and any indexed family of elements $f : \iota \to \alpha$, the element $a$ is disjoint from the supremum $\bigsqcup_i f_i$ if and only if $a$ is disjoint from $f_i$ for every $i \in \iota$. In symbols: \[ a \perp \bigsqcup_i f_i \leftrightarrow \forall i, a \perp f_i. \]

iSup₂_disjoint_iff theorem

{f : ∀ i, κ i → α} : Disjoint (⨆ (i) (j), f i j) a ↔ ∀ i j, Disjoint (f i j) a

Full source

theorem iSup₂_disjoint_iff {f : ∀ i, κ i → α} :
    DisjointDisjoint (⨆ (i) (j), f i j) a ↔ ∀ i j, Disjoint (f i j) a := by
  simp_rw [iSup_disjoint_iff]

Disjointness of Doubly Indexed Supremum: $\bigsqcup_{i,j} f_{i,j} \perp a \leftrightarrow \forall i j, f_{i,j} \perp a$

Informal description

For any doubly indexed family of elements $f_{i,j}$ in a frame $\alpha$ and any element $a \in \alpha$, the supremum $\bigsqcup_{i,j} f_{i,j}$ is disjoint from $a$ if and only if $f_{i,j}$ is disjoint from $a$ for every $i$ and $j$.

disjoint_iSup₂_iff theorem

{f : ∀ i, κ i → α} : Disjoint a (⨆ (i) (j), f i j) ↔ ∀ i j, Disjoint a (f i j)

Full source

theorem disjoint_iSup₂_iff {f : ∀ i, κ i → α} :
    DisjointDisjoint a (⨆ (i) (j), f i j) ↔ ∀ i j, Disjoint a (f i j) := by
  simp_rw [disjoint_iSup_iff]

Disjointness with Doubly Indexed Supremum in a Frame

Informal description

For any element $a$ in a frame $\alpha$ and any doubly indexed family of elements $f : \forall i, \kappa_i \to \alpha$, the element $a$ is disjoint from the supremum $\bigsqcup_{i,j} f_i(j)$ if and only if $a$ is disjoint from $f_i(j)$ for every $i$ and $j$. In symbols: \[ a \perp \bigsqcup_{i,j} f_i(j) \leftrightarrow \forall i\, j, a \perp f_i(j). \]

sSup_disjoint_iff theorem

{s : Set α} : Disjoint (sSup s) a ↔ ∀ b ∈ s, Disjoint b a

Full source

theorem sSup_disjoint_iff {s : Set α} : DisjointDisjoint (sSup s) a ↔ ∀ b ∈ s, Disjoint b a := by
  simp only [disjoint_iff, sSup_inf_eq, iSup_eq_bot]

Disjointness of Supremum in a Frame: $\bigsqcup s \perp a \leftrightarrow \forall b \in s, b \perp a$

Informal description

For any subset $s$ of a frame $\alpha$ and any element $a \in \alpha$, the supremum $\bigsqcup s$ is disjoint from $a$ if and only if every element $b \in s$ is disjoint from $a$. In symbols: \[ \left(\bigsqcup s\right) \perp a \leftrightarrow \forall b \in s, b \perp a. \]

disjoint_sSup_iff theorem

{s : Set α} : Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b

Full source

theorem disjoint_sSup_iff {s : Set α} : DisjointDisjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b := by
  simpa only [disjoint_comm] using @sSup_disjoint_iff

Disjointness with Supremum in a Frame: $a \perp \bigsqcup s \leftrightarrow \forall b \in s, a \perp b$

Informal description

For any subset $s$ of a frame $\alpha$ and any element $a \in \alpha$, the element $a$ is disjoint from the supremum $\bigsqcup s$ if and only if $a$ is disjoint from every element $b \in s$. In symbols: \[ a \perp \bigsqcup s \leftrightarrow \forall b \in s, a \perp b. \]

iSup_inf_of_monotone theorem

 {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → α} (hf : Monotone f) (hg : Monotone g) :
  ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i

Full source

theorem iSup_inf_of_monotone {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → α}
    (hf : Monotone f) (hg : Monotone g) : ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i := by
  refine (le_iSup_inf_iSup f g).antisymm ?_
  rw [iSup_inf_iSup]
  refine iSup_mono' fun i => ?_
  rcases directed_of (· ≤ ·) i.1 i.2 with ⟨j, h₁, h₂⟩
  exact ⟨j, inf_le_inf (hf h₁) (hg h₂)⟩

Supremum of Meets of Monotone Functions Equals Meet of Suprema in Frames

Informal description

Let $\alpha$ be a frame, $\iota$ a preorder directed with respect to $\leq$, and $f, g : \iota \to \alpha$ monotone functions. Then the supremum of the pairwise meets equals the meet of the suprema: \[ \bigsqcup_{i} (f_i \sqcap g_i) = \left(\bigsqcup_{i} f_i\right) \sqcap \left(\bigsqcup_{i} g_i\right). \]

iSup_inf_of_antitone theorem

 {ι : Type*} [Preorder ι] [IsDirected ι (swap (· ≤ ·))] {f g : ι → α} (hf : Antitone f) (hg : Antitone g) :
  ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i

Full source

theorem iSup_inf_of_antitone {ι : Type*} [Preorder ι] [IsDirected ι (swap (· ≤ ·))] {f g : ι → α}
    (hf : Antitone f) (hg : Antitone g) : ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i :=
  @iSup_inf_of_monotone α _ ιᵒᵈ _ _ f g hf.dual_left hg.dual_left

Supremum of Meets of Antitone Functions Equals Meet of Suprema in Frames

Informal description

Let $\alpha$ be a frame, $\iota$ a preorder directed with respect to $\geq$, and $f, g : \iota \to \alpha$ antitone functions. Then the supremum of the pairwise meets equals the meet of the suprema: \[ \bigsqcup_{i} (f_i \sqcap g_i) = \left(\bigsqcup_{i} f_i\right) \sqcap \left(\bigsqcup_{i} g_i\right). \]

himp_eq_sSup theorem

: a ⇨ b = sSup {w | w ⊓ a ≤ b}

Full source

theorem himp_eq_sSup : a ⇨ b = sSup {w | w ⊓ a ≤ b} :=
  (isGreatest_himp a b).isLUB.sSup_eq.symm

Heyting Implication as Supremum: $a \Rightarrow b = \bigsqcup \{w \mid w \sqcap a \leq b\}$

Informal description

In a frame (complete Heyting algebra) $\alpha$, the Heyting implication $a \Rightarrow b$ is equal to the supremum of the set $\{w \in \alpha \mid w \sqcap a \leq b\}$.

compl_eq_sSup_disjoint theorem

: aᶜ = sSup {w | Disjoint w a}

Full source

theorem compl_eq_sSup_disjoint : aᶜ = sSup {w | Disjoint w a} :=
  (isGreatest_compl a).isLUB.sSup_eq.symm

Pseudo-complement as Supremum of Disjoint Elements

Informal description

In a frame (complete Heyting algebra) $\alpha$, the pseudo-complement $\neg a$ of an element $a \in \alpha$ is equal to the supremum of the set $\{w \in \alpha \mid w \text{ is disjoint from } a\}$.

himp_le_iff theorem

: a ⇨ b ≤ c ↔ ∀ d, d ⊓ a ≤ b → d ≤ c

Full source

lemma himp_le_iff : a ⇨ ba ⇨ b ≤ c ↔ ∀ d, d ⊓ a ≤ b → d ≤ c := by simp [himp_eq_sSup]

Characterization of Heyting Implication via Upper Bounds: $a \Rightarrow b \leq c \iff (\forall d, d \sqcap a \leq b \to d \leq c)$

Informal description

In a frame (complete Heyting algebra) $\alpha$, for any elements $a, b, c \in \alpha$, the Heyting implication $a \Rightarrow b$ is less than or equal to $c$ if and only if for every element $d \in \alpha$ satisfying $d \sqcap a \leq b$, we have $d \leq c$.

Frame.toDistribLattice instance

: DistribLattice α

Full source

instance (priority := 100) Frame.toDistribLattice : DistribLattice α :=
  DistribLattice.ofInfSupLe fun a b c => by
    rw [← sSup_pair, ← sSup_pair, inf_sSup_eq, ← sSup_image, image_pair]

Frames are Distributive Lattices

Informal description

Every frame $\alpha$ is a distributive lattice. That is, finite meets $\sqcap$ distribute over finite joins $\sqcup$ in $\alpha$.

Prod.instFrame instance

[Frame α] [Frame β] : Frame (α × β)

Full source

instance Prod.instFrame [Frame α] [Frame β] : Frame (α × β) where
  __ := instCompleteLattice
  __ := instHeytingAlgebra

Frame Structure on Product Types

Informal description

For any two frames $\alpha$ and $\beta$, the product $\alpha \times \beta$ is also a frame, with the meet and join operations defined componentwise. That is, the finite meets $\sqcap$ distribute over arbitrary joins $\bigsqcup$ in each component.

Pi.instFrame instance

{ι : Type*} {π : ι → Type*} [∀ i, Frame (π i)] : Frame (∀ i, π i)

Full source

instance Pi.instFrame {ι : Type*} {π : ι → Type*} [∀ i, Frame (π i)] : Frame (∀ i, π i) where
  __ := instCompleteLattice
  __ := instHeytingAlgebra

Pointwise Frame Structure on Product Types

Informal description

For any family of frames $(\pi_i)_{i \in \iota}$ indexed by a type $\iota$, the product type $\forall i, \pi_i$ is also a frame, with the frame structure defined pointwise. That is, the meet, join, and Heyting implication operations are defined componentwise, and the infinite distributivity law holds in each component.

OrderDual.instFrame instance

: Frame αᵒᵈ

Full source

instance OrderDual.instFrame : Frame αᵒᵈ where
  __ := instCompleteLattice
  __ := instHeytingAlgebra

Order Dual of a Frame is a Frame

Informal description

For any frame $\alpha$, the order dual $\alpha^{\text{op}}$ is also a frame. That is, the complete lattice obtained by reversing the order of $\alpha$ satisfies the frame condition where finite meets distribute over arbitrary joins in the dual order.

sInf_sup_eq theorem

: sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b

Full source

theorem sInf_sup_eq : sInfsInf s ⊔ b = ⨅ a ∈ s, a ⊔ b :=
  @sSup_inf_eq αᵒᵈ _ _ _

Infimum-Join Distributivity in Coframes

Informal description

In a coframe $\alpha$, for any subset $s \subseteq \alpha$ and any element $b \in \alpha$, the join of the infimum of $s$ with $b$ equals the infimum of the joins of each element of $s$ with $b$. That is, \[ \left( \bigsqcap s \right) \sqcup b = \bigsqcap_{a \in s} (a \sqcup b). \]

iInf_sup_eq theorem

(f : ι → α) (a : α) : (⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a

Full source

theorem iInf_sup_eq (f : ι → α) (a : α) : (⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a :=
  @iSup_inf_eq αᵒᵈ _ _ _ _

Distributivity of Join over Indexed Infimum in Coframes

Informal description

In a coframe $\alpha$, for any indexed family of elements $f : \iota \to \alpha$ and any element $a \in \alpha$, the join of the infimum of $f$ with $a$ equals the infimum of the joins of each $f_i$ with $a$. That is, \[ \left( \bigsqcap_{i} f_i \right) \sqcup a = \bigsqcap_{i} (f_i \sqcup a). \]

sup_iInf_eq theorem

(a : α) (f : ι → α) : (a ⊔ ⨅ i, f i) = ⨅ i, a ⊔ f i

Full source

theorem sup_iInf_eq (a : α) (f : ι → α) : (a ⊔ ⨅ i, f i) = ⨅ i, a ⊔ f i :=
  @inf_iSup_eq αᵒᵈ _ _ _ _

Finite Join Distributes over Infinite Infimum in Coframes

Informal description

In a coframe $\alpha$, for any element $a \in \alpha$ and any indexed family of elements $f : \iota \to \alpha$, the join of $a$ with the infimum of $f$ equals the infimum of the joins of $a$ with each $f_i$. That is, \[ a \sqcup \left( \bigsqcap_{i} f_i \right) = \bigsqcap_{i} (a \sqcup f_i). \]

iInf₂_sup_eq theorem

{f : ∀ i, κ i → α} (a : α) : (⨅ (i) (j), f i j) ⊔ a = ⨅ (i) (j), f i j ⊔ a

Full source

theorem iInf₂_sup_eq {f : ∀ i, κ i → α} (a : α) : (⨅ (i) (j), f i j) ⊔ a = ⨅ (i) (j), f i j ⊔ a :=
  @iSup₂_inf_eq αᵒᵈ _ _ _ _ _

Distributivity of Join over Doubly Indexed Infimum in Coframes

Informal description

Let $\alpha$ be a coframe and let $f : \forall i, \kappa_i \to \alpha$ be a doubly indexed family of elements in $\alpha$. For any element $a \in \alpha$, the join of the infimum of $f$ with $a$ equals the infimum of the joins of each $f_{i,j}$ with $a$. That is, \[ \left( \bigsqcap_{i,j} f_{i,j} \right) \sqcup a = \bigsqcap_{i,j} (f_{i,j} \sqcup a). \]

sup_iInf₂_eq theorem

{f : ∀ i, κ i → α} (a : α) : (a ⊔ ⨅ (i) (j), f i j) = ⨅ (i) (j), a ⊔ f i j

Full source

theorem sup_iInf₂_eq {f : ∀ i, κ i → α} (a : α) : (a ⊔ ⨅ (i) (j), f i j) = ⨅ (i) (j), a ⊔ f i j :=
  @inf_iSup₂_eq αᵒᵈ _ _ _ _ _

Distributivity of Join over Doubly Indexed Infimum in Coframes

Informal description

In a coframe $\alpha$, for any element $a \in \alpha$ and any doubly indexed family of elements $f : \forall i, \kappa_i \to \alpha$, the join of $a$ with the infimum of $f$ equals the infimum of the joins of $a$ with each $f_{i,j}$. That is, \[ a \sqcup \left( \bigsqcap_{i,j} f_{i,j} \right) = \bigsqcap_{i,j} (a \sqcup f_{i,j}). \]

iInf_sup_iInf theorem

{ι ι' : Type*} {f : ι → α} {g : ι' → α} : ((⨅ i, f i) ⊔ ⨅ i, g i) = ⨅ i : ι × ι', f i.1 ⊔ g i.2

Full source

theorem iInf_sup_iInf {ι ι' : Type*} {f : ι → α} {g : ι' → α} :
    ((⨅ i, f i) ⊔ ⨅ i, g i) = ⨅ i : ι × ι', f i.1 ⊔ g i.2 :=
  @iSup_inf_iSup αᵒᵈ _ _ _ _ _

Distributivity of Join over Infima in Coframes: $\left( \bigsqcap_i f_i \right) \sqcup \left( \bigsqcap_j g_j \right) = \bigsqcap_{i,j} (f_i \sqcup g_j)$

Informal description

Let $\alpha$ be a coframe, and let $f : \iota \to \alpha$ and $g : \iota' \to \alpha$ be two indexed families of elements in $\alpha$. Then the join of their infima equals the infimum of the pairwise joins over the product index type. That is, \[ \left( \bigsqcap_{i} f_i \right) \sqcup \left( \bigsqcap_{j} g_j \right) = \bigsqcap_{(i,j) \in \iota \times \iota'} (f_i \sqcup g_j). \]

biInf_sup_biInf theorem

 {ι ι' : Type*} {f : ι → α} {g : ι' → α} {s : Set ι} {t : Set ι'} :
  ((⨅ i ∈ s, f i) ⊔ ⨅ j ∈ t, g j) = ⨅ p ∈ s ×ˢ t, f (p : ι × ι').1 ⊔ g p.2

Full source

theorem biInf_sup_biInf {ι ι' : Type*} {f : ι → α} {g : ι' → α} {s : Set ι} {t : Set ι'} :
    ((⨅ i ∈ s, f i) ⊔ ⨅ j ∈ t, g j) = ⨅ p ∈ s ×ˢ t, f (p : ι × ι').1 ⊔ g p.2 :=
  @biSup_inf_biSup αᵒᵈ _ _ _ _ _ _ _

Distributivity of Join over Bounded Infima in Coframes: $\left( \bigsqcap_{i \in s} f_i \right) \sqcup \left( \bigsqcap_{j \in t} g_j \right) = \bigsqcap_{(i,j) \in s \times t} (f_i \sqcup g_j)$

Informal description

Let $\alpha$ be a coframe, and let $f : \iota \to \alpha$ and $g : \iota' \to \alpha$ be two indexed families of elements in $\alpha$, with $s \subseteq \iota$ and $t \subseteq \iota'$ subsets of their respective index sets. Then the join of the bounded infima of $f$ over $s$ and $g$ over $t$ equals the infimum of the pairwise joins over the product set $s \times t$. That is, \[ \left( \bigsqcap_{i \in s} f_i \right) \sqcup \left( \bigsqcap_{j \in t} g_j \right) = \bigsqcap_{(i,j) \in s \times t} (f_i \sqcup g_j). \]

sInf_sup_sInf theorem

: sInf s ⊔ sInf t = ⨅ p ∈ s ×ˢ t, (p : α × α).1 ⊔ p.2

Full source

theorem sInf_sup_sInf : sInfsInf s ⊔ sInf t = ⨅ p ∈ s ×ˢ t, (p : α × α).1 ⊔ p.2 :=
  @sSup_inf_sSup αᵒᵈ _ _ _

Distributivity of Join over Infima in Coframes: $\left( \bigsqcap_{a \in s} a \right) \sqcup \left( \bigsqcap_{b \in t} b \right) = \bigsqcap_{(a,b) \in s \times t} (a \sqcup b)$

Informal description

Let $\alpha$ be a coframe, and let $s, t \subseteq \alpha$ be subsets of $\alpha$. Then the join of their infima equals the infimum of the pairwise joins over the product set $s \times t$. That is, \[ \left( \bigsqcap_{a \in s} a \right) \sqcup \left( \bigsqcap_{b \in t} b \right) = \bigsqcap_{(a,b) \in s \times t} (a \sqcup b). \]

iInf_sup_of_monotone theorem

 {ι : Type*} [Preorder ι] [IsDirected ι (swap (· ≤ ·))] {f g : ι → α} (hf : Monotone f) (hg : Monotone g) :
  ⨅ i, f i ⊔ g i = (⨅ i, f i) ⊔ ⨅ i, g i

Full source

theorem iInf_sup_of_monotone {ι : Type*} [Preorder ι] [IsDirected ι (swap (· ≤ ·))] {f g : ι → α}
    (hf : Monotone f) (hg : Monotone g) : ⨅ i, f i ⊔ g i = (⨅ i, f i) ⊔ ⨅ i, g i :=
  @iSup_inf_of_antitone αᵒᵈ _ _ _ _ _ _ hf.dual_right hg.dual_right

Infimum of Joins of Monotone Functions Equals Join of Infima in Coframes

Informal description

Let $\alpha$ be a coframe, $\iota$ a preorder directed with respect to $\geq$, and $f, g : \iota \to \alpha$ monotone functions. Then the infimum of the pairwise joins equals the join of the infima: \[ \bigsqcap_{i} (f_i \sqcup g_i) = \left(\bigsqcap_{i} f_i\right) \sqcup \left(\bigsqcap_{i} g_i\right). \]

iInf_sup_of_antitone theorem

 {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → α} (hf : Antitone f) (hg : Antitone g) :
  ⨅ i, f i ⊔ g i = (⨅ i, f i) ⊔ ⨅ i, g i

Full source

theorem iInf_sup_of_antitone {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → α}
    (hf : Antitone f) (hg : Antitone g) : ⨅ i, f i ⊔ g i = (⨅ i, f i) ⊔ ⨅ i, g i :=
  @iSup_inf_of_monotone αᵒᵈ _ _ _ _ _ _ hf.dual_right hg.dual_right

Infimum of Joins of Antitone Functions Equals Join of Infima in Coframes

Informal description

Let $\alpha$ be a coframe, $\iota$ a preorder directed with respect to $\leq$, and $f, g : \iota \to \alpha$ antitone functions. Then the infimum of the pairwise joins equals the join of the infima: \[ \bigsqcap_{i} (f_i \sqcup g_i) = \left(\bigsqcap_{i} f_i\right) \sqcup \left(\bigsqcap_{i} g_i\right). \]

sdiff_eq_sInf theorem

: a \ b = sInf {w | a ≤ b ⊔ w}

Full source

theorem sdiff_eq_sInf : a \ b = sInf {w | a ≤ b ⊔ w} :=
  (isLeast_sdiff a b).isGLB.sInf_eq.symm

Difference as Infimum Characterization in Coframes: $a \setminus b = \bigsqcap \{w \mid a \leq b \sqcup w\}$

Informal description

In a coframe (complete co-Heyting algebra) $\alpha$, the difference $a \setminus b$ of two elements $a, b \in \alpha$ is equal to the infimum of the set $\{w \in \alpha \mid a \leq b \sqcup w\}$.

hnot_eq_sInf_codisjoint theorem

: ￢a = sInf {w | Codisjoint a w}

Full source

theorem hnot_eq_sInf_codisjoint : ￢a = sInf {w | Codisjoint a w} :=
  (isLeast_hnot a).isGLB.sInf_eq.symm

Negation as Infimum of Codisjoint Elements in Coframe: $\neg a = \bigsqcap \{w \mid a \sqcup w = \top\}$

Informal description

In a coframe $\alpha$, the negation $\neg a$ of an element $a \in \alpha$ is equal to the infimum of the set $\{w \in \alpha \mid \text{Codisjoint}(a, w)\}$, where $\text{Codisjoint}(a, w)$ means $a \sqcup w = \top$.

le_sdiff_iff theorem

: a ≤ b \ c ↔ ∀ d, b ≤ c ⊔ d → a ≤ d

Full source

lemma le_sdiff_iff : a ≤ b \ c ↔ ∀ d, b ≤ c ⊔ d → a ≤ d := by simp [sdiff_eq_sInf]

Characterization of Difference Order in Coframes: $a \leq b \setminus c \leftrightarrow (\forall d, b \leq c \sqcup d \to a \leq d)$

Informal description

For elements $a, b, c$ in a coframe, $a \leq b \setminus c$ if and only if for every element $d$, if $b \leq c \sqcup d$ then $a \leq d$.

Coframe.toDistribLattice instance

: DistribLattice α

Full source

instance (priority := 100) Coframe.toDistribLattice : DistribLattice α where
  __ := ‹Coframe α›
  le_sup_inf a b c := by
    rw [← sInf_pair, ← sInf_pair, sup_sInf_eq, ← sInf_image, image_pair]

Coframes are Distributive Lattices

Informal description

Every coframe is a distributive lattice. In other words, a complete lattice where the join operation $\sqcup$ distributes over arbitrary meets $\bigsqcap$ also satisfies the finite distributivity condition for join and meet operations.

Prod.instCoframe instance

[Coframe β] : Coframe (α × β)

Full source

instance Prod.instCoframe [Coframe β] : Coframe (α × β) where
  __ := instCompleteLattice
  __ := instCoheytingAlgebra

Product of Coframes is a Coframe

Informal description

For any two coframes $\alpha$ and $\beta$, the product $\alpha \times \beta$ is also a coframe, where the meet and join operations are defined componentwise.

Pi.instCoframe instance

{ι : Type*} {π : ι → Type*} [∀ i, Coframe (π i)] : Coframe (∀ i, π i)

Full source

instance Pi.instCoframe {ι : Type*} {π : ι → Type*} [∀ i, Coframe (π i)] : Coframe (∀ i, π i) where
  __ := instCompleteLattice
  __ := instCoheytingAlgebra

Pointwise Coframe Structure on Product Types

Informal description

For any family of types $(\pi_i)_{i \in \iota}$ where each $\pi_i$ is a coframe, the product type $\forall i, \pi_i$ is also a coframe, with the lattice operations defined pointwise.

OrderDual.instCompleteDistribLattice instance

[CompleteDistribLattice α] : CompleteDistribLattice αᵒᵈ

Full source

instance OrderDual.instCompleteDistribLattice [CompleteDistribLattice α] :
    CompleteDistribLattice αᵒᵈ where
  __ := instFrame
  __ := instCoframe

Order Dual of a Complete Distributive Lattice is Complete Distributive

Informal description

For any complete distributive lattice $\alpha$, the order dual $\alpha^{\text{op}}$ is also a complete distributive lattice. That is, the complete lattice obtained by reversing the order of $\alpha$ satisfies the complete distributivity conditions where finite meets distribute over arbitrary joins and finite joins distribute over arbitrary meets in the dual order.

Prod.instCompleteDistribLattice instance

[CompleteDistribLattice β] : CompleteDistribLattice (α × β)

Full source

instance Prod.instCompleteDistribLattice [CompleteDistribLattice β] :
    CompleteDistribLattice (α × β) where
  __ := instFrame
  __ := instCoframe

Product of Complete Distributive Lattices is Complete Distributive

Informal description

For any two complete distributive lattices $\alpha$ and $\beta$, the product $\alpha \times \beta$ is also a complete distributive lattice, with the meet and join operations defined componentwise.

Pi.instCompleteDistribLattice instance

{ι : Type*} {π : ι → Type*} [∀ i, CompleteDistribLattice (π i)] : CompleteDistribLattice (∀ i, π i)

Full source

instance Pi.instCompleteDistribLattice {ι : Type*} {π : ι → Type*}
    [∀ i, CompleteDistribLattice (π i)] : CompleteDistribLattice (∀ i, π i) where
  __ := instFrame
  __ := instCoframe

Pointwise Complete Distributive Lattice Structure on Product Types

Informal description

For any family of types $(\pi_i)_{i \in \iota}$ where each $\pi_i$ is a complete distributive lattice, the product type $\forall i, \pi_i$ is also a complete distributive lattice, with the lattice operations defined pointwise.

OrderDual.instCompletelyDistribLattice instance

[CompletelyDistribLattice α] : CompletelyDistribLattice αᵒᵈ

Full source

instance OrderDual.instCompletelyDistribLattice [CompletelyDistribLattice α] :
    CompletelyDistribLattice αᵒᵈ where
  __ := instFrame
  __ := instCoframe
  iInf_iSup_eq _ := iSup_iInf_eq (α := α)

Order Dual of a Completely Distributive Lattice is Completely Distributive

Informal description

For any completely distributive lattice $\alpha$, the order dual $\alpha^{\text{op}}$ is also a completely distributive lattice. That is, reversing the order of a completely distributive lattice preserves the property that arbitrary meets and joins distribute over each other.

Prod.instCompletelyDistribLattice instance

[CompletelyDistribLattice α] [CompletelyDistribLattice β] : CompletelyDistribLattice (α × β)

Full source

instance Prod.instCompletelyDistribLattice [CompletelyDistribLattice α]
    [CompletelyDistribLattice β] : CompletelyDistribLattice (α × β) where
  __ := instFrame
  __ := instCoframe
  iInf_iSup_eq f := by ext <;> simp [fst_iSup, fst_iInf, snd_iSup, snd_iInf, iInf_iSup_eq]

Product of Completely Distributive Lattices is Completely Distributive

Informal description

For any two completely distributive lattices $\alpha$ and $\beta$, the product $\alpha \times \beta$ is also a completely distributive lattice, with meet and join operations defined componentwise.

Pi.instCompletelyDistribLattice instance

{ι : Type*} {π : ι → Type*} [∀ i, CompletelyDistribLattice (π i)] : CompletelyDistribLattice (∀ i, π i)

Full source

instance Pi.instCompletelyDistribLattice {ι : Type*} {π : ι → Type*}
    [∀ i, CompletelyDistribLattice (π i)] : CompletelyDistribLattice (∀ i, π i) where
  __ := instFrame
  __ := instCoframe
  iInf_iSup_eq f := by ext i; simp only [iInf_apply, iSup_apply, iInf_iSup_eq]

Pointwise Completely Distributive Lattice Structure on Product Types

Informal description

For any family of types $(\pi_i)_{i \in \iota}$ where each $\pi_i$ is a completely distributive lattice, the product type $\forall i, \pi_i$ is also a completely distributive lattice, with the lattice operations defined pointwise. This means that the infinite meet and join operations satisfy the complete distributivity condition: \[ \bigsqcap_{a} \bigsqcup_{b} f(a, b) = \bigsqcup_{g} \bigsqcap_{a} f(a, g(a)) \] for any family of elements $f(a, b)$ in the product lattice.

CompleteBooleanAlgebra structure

(α) extends CompleteLattice α, BooleanAlgebra α

Full source

/--
A complete Boolean algebra is a Boolean algebra that is also a complete distributive lattice.

It is only completely distributive if it is also atomic.
-/
-- We do not directly extend `CompleteDistribLattice` to avoid having the `hnot` field
class CompleteBooleanAlgebra (α) extends CompleteLattice α, BooleanAlgebra α where
  /-- `⊓` distributes over `⨆`. -/
  inf_sSup_le_iSup_inf (a : α) (s : Set α) : a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
  /-- `⊔` distributes over `⨅`. -/
  iInf_sup_le_sup_sInf (a : α) (s : Set α) : ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

Complete Boolean Algebra

Informal description

A complete Boolean algebra is a Boolean algebra that is also a complete lattice, where finite meets (infima) distribute over arbitrary joins (suprema) and finite joins distribute over arbitrary meets. This means that for any element $ a $ and any family of elements $ (f_i)_{i \in I} $, the following distributive laws hold: \[ a \sqcap \left( \bigsqcup_{i} f_i \right) = \bigsqcup_{i} (a \sqcap f_i) \] \[ a \sqcup \left( \bigsqcap_{i} f_i \right) = \bigsqcap_{i} (a \sqcup f_i) \] Additionally, a complete Boolean algebra is completely distributive if it satisfies the stronger condition that arbitrary meets distribute over arbitrary joins: \[ \bigsqcap_{i} \left( \bigsqcup_{j} f_{i,j} \right) = \bigsqcup_{s} \left( \bigsqcap_{i} f_{i, s(i)} \right) \] where $ s $ ranges over all choice functions. This property holds if the algebra is atomic.

CompleteBooleanAlgebra.toCompleteDistribLattice instance

[CompleteBooleanAlgebra α] : CompleteDistribLattice α

Full source

instance (priority := 100) CompleteBooleanAlgebra.toCompleteDistribLattice
    [CompleteBooleanAlgebra α] : CompleteDistribLattice α where
  __ := ‹CompleteBooleanAlgebra α›
  __ := BooleanAlgebra.toBiheytingAlgebra

Complete Boolean Algebras are Complete Distributive Lattices

Informal description

Every complete Boolean algebra is a complete distributive lattice. That is, for any complete Boolean algebra $\alpha$, the lattice operations satisfy both finite meets distributing over arbitrary joins and finite joins distributing over arbitrary meets: \[ a \sqcap \left( \bigsqcup_{i} f_i \right) = \bigsqcup_{i} (a \sqcap f_i) \] \[ a \sqcup \left( \bigsqcap_{i} f_i \right) = \bigsqcap_{i} (a \sqcup f_i) \]

Prod.instCompleteBooleanAlgebra instance

[CompleteBooleanAlgebra α] [CompleteBooleanAlgebra β] : CompleteBooleanAlgebra (α × β)

Full source

instance Prod.instCompleteBooleanAlgebra [CompleteBooleanAlgebra α] [CompleteBooleanAlgebra β] :
    CompleteBooleanAlgebra (α × β) where
  __ := instBooleanAlgebra
  __ := instCompleteDistribLattice
  inf_sSup_le_iSup_inf _ _ := inf_sSup_eq.le
  iInf_sup_le_sup_sInf _ _ := sup_sInf_eq.ge

Componentwise Complete Boolean Algebra Structure on Products

Informal description

For any two complete Boolean algebras $\alpha$ and $\beta$, the product $\alpha \times \beta$ is also a complete Boolean algebra, with all operations defined componentwise. Specifically: - The meet operation is $(a_1, b_1) \sqcap (a_2, b_2) = (a_1 \sqcap a_2, b_1 \sqcap b_2)$, - The join operation is $(a_1, b_1) \sqcup (a_2, b_2) = (a_1 \sqcup a_2, b_1 \sqcup b_2)$, - The complement operation is $(a, b)^\complement = (a^\complement, b^\complement)$, - The top element is $(\top, \top)$, - The bottom element is $(\bot, \bot)$.

Pi.instCompleteBooleanAlgebra instance

{ι : Type*} {π : ι → Type*} [∀ i, CompleteBooleanAlgebra (π i)] : CompleteBooleanAlgebra (∀ i, π i)

Full source

instance Pi.instCompleteBooleanAlgebra {ι : Type*} {π : ι → Type*}
    [∀ i, CompleteBooleanAlgebra (π i)] : CompleteBooleanAlgebra (∀ i, π i) where
  __ := instBooleanAlgebra
  __ := instCompleteDistribLattice
  inf_sSup_le_iSup_inf _ _ := inf_sSup_eq.le
  iInf_sup_le_sup_sInf _ _ := sup_sInf_eq.ge

Pointwise Complete Boolean Algebra Structure on Product Types

Informal description

For any family of types $(\pi_i)_{i \in \iota}$ where each $\pi_i$ is a complete Boolean algebra, the product type $\prod_{i \in \iota} \pi_i$ is also a complete Boolean algebra, with all operations (meet $\sqcap$, join $\sqcup$, complement $(\cdot)^\complement$, set difference $\setminus$, Heyting implication $\Rightarrow$, top $\top$, and bottom $\bot$) defined pointwise. Specifically: 1. $(f \sqcap g)(i) = f(i) \sqcap g(i)$, 2. $(f \sqcup g)(i) = f(i) \sqcup g(i)$, 3. $f^\complement(i) = (f(i))^\complement$, 4. $(f \setminus g)(i) = f(i) \setminus g(i)$, 5. $(f \Rightarrow g)(i) = f(i) \Rightarrow g(i)$, 6. $\top(i) = \top$, 7. $\bot(i) = \bot$, for all $i \in \iota$ and $f, g \in \prod_{i \in \iota} \pi_i$.

OrderDual.instCompleteBooleanAlgebra instance

[CompleteBooleanAlgebra α] : CompleteBooleanAlgebra αᵒᵈ

Full source

instance OrderDual.instCompleteBooleanAlgebra [CompleteBooleanAlgebra α] :
    CompleteBooleanAlgebra αᵒᵈ where
  __ := instBooleanAlgebra
  __ := instCompleteDistribLattice
  inf_sSup_le_iSup_inf _ _ := inf_sSup_eq.le
  iInf_sup_le_sup_sInf _ _ := sup_sInf_eq.ge

Order Dual of a Complete Boolean Algebra is Complete Boolean

Informal description

For any complete Boolean algebra $\alpha$, the order dual $\alpha^{\text{op}}$ is also a complete Boolean algebra. In this dual structure, the meet and join operations are swapped, and the complement operation remains unchanged.

compl_iInf theorem

: (iInf f)ᶜ = ⨆ i, (f i)ᶜ

Full source

theorem compl_iInf : (iInf f)ᶜ = ⨆ i, (f i)ᶜ :=
  le_antisymm
    (compl_le_of_compl_le <| le_iInf fun i => compl_le_of_compl_le <|
      le_iSup (HasCompl.complHasCompl.compl ∘ f) i)
    (iSup_le fun _ => compl_le_compl <| iInf_le _ _)

De Morgan's Law for Infima: $\left( \bigsqcap_i f_i \right)^\complement = \bigsqcup_i f_i^\complement$

Informal description

In a complete Boolean algebra, the complement of the infimum of a family of elements $(f_i)_{i \in I}$ is equal to the supremum of their complements, i.e., \[ \left( \bigsqcap_{i} f_i \right)^\complement = \bigsqcup_{i} (f_i)^\complement. \]

compl_iSup theorem

: (iSup f)ᶜ = ⨅ i, (f i)ᶜ

Full source

theorem compl_iSup : (iSup f)ᶜ = ⨅ i, (f i)ᶜ :=
  compl_injective (by simp [compl_iInf])

De Morgan's Law for Suprema: $\left( \bigsqcup_i f_i \right)^\complement = \bigsqcap_i f_i^\complement$

Informal description

In a complete Boolean algebra, the complement of the supremum of a family of elements $(f_i)_{i \in I}$ is equal to the infimum of their complements, i.e., \[ \left( \bigsqcup_{i} f_i \right)^\complement = \bigsqcap_{i} (f_i)^\complement. \]

compl_sInf theorem

: (sInf s)ᶜ = ⨆ i ∈ s, iᶜ

Full source

theorem compl_sInf : (sInf s)ᶜ = ⨆ i ∈ s, iᶜ := by simp only [sInf_eq_iInf, compl_iInf]

De Morgan's Law for Set Infima: $\left( \bigsqcap s \right)^\complement = \bigsqcup_{i \in s} i^\complement$

Informal description

In a complete Boolean algebra, the complement of the infimum of a set $s$ is equal to the supremum of the complements of all elements in $s$, i.e., \[ \left( \bigsqcap_{i \in s} i \right)^\complement = \bigsqcup_{i \in s} i^\complement. \]

compl_sSup theorem

: (sSup s)ᶜ = ⨅ i ∈ s, iᶜ

Full source

theorem compl_sSup : (sSup s)ᶜ = ⨅ i ∈ s, iᶜ := by simp only [sSup_eq_iSup, compl_iSup]

De Morgan's Law for Set Suprema: $\left( \bigsqcup s \right)^\complement = \bigsqcap_{i \in s} i^\complement$

Informal description

In a complete Boolean algebra, the complement of the supremum of a set $s$ is equal to the infimum of the complements of all elements in $s$, i.e., \[ \left( \bigsqcup_{i \in s} i \right)^\complement = \bigsqcap_{i \in s} i^\complement. \]

compl_sInf' theorem

: (sInf s)ᶜ = sSup (HasCompl.compl '' s)

Full source

theorem compl_sInf' : (sInf s)ᶜ = sSup (HasCompl.complHasCompl.compl '' s) :=
  compl_sInf.trans sSup_image.symm

De Morgan's Law for Set Infima via Image: $\left( \bigsqcap s \right)^\complement = \bigsqcup \{\, i^\complement \mid i \in s \,\}$

Informal description

In a complete Boolean algebra, the complement of the infimum of a set $s$ is equal to the supremum of the image of $s$ under the complement operation, i.e., \[ \left( \bigsqcap s \right)^\complement = \bigsqcup \{ i^\complement \mid i \in s \}. \]

compl_sSup' theorem

: (sSup s)ᶜ = sInf (HasCompl.compl '' s)

Full source

theorem compl_sSup' : (sSup s)ᶜ = sInf (HasCompl.complHasCompl.compl '' s) :=
  compl_sSup.trans sInf_image.symm

De Morgan's Law for Suprema via Complement Image: $\left( \bigsqcup s \right)^\complement = \bigsqcap \{\, i^\complement \mid i \in s \,\}$

Informal description

In a complete Boolean algebra, the complement of the supremum of a set $s$ is equal to the infimum of the set of complements of elements in $s$, i.e., \[ \left( \bigsqcup s \right)^\complement = \bigsqcap \{ i^\complement \mid i \in s \}. \]

iSup_symmDiff_iSup_le theorem

{g : ι → α} : (⨆ i, f i) ∆ (⨆ i, g i) ≤ ⨆ i, ((f i) ∆ (g i))

Full source

/-- The symmetric difference of two `iSup`s is at most the `iSup` of the symmetric differences. -/
theorem iSup_symmDiff_iSup_le {g : ι → α} : (⨆ i, f i) ∆ (⨆ i, g i) ≤ ⨆ i, ((f i) ∆ (g i)) := by
  simp_rw [symmDiff_le_iff, ← iSup_sup_eq]
  exact ⟨iSup_mono fun i ↦ sup_comm (g i) _ ▸ le_symmDiff_sup_right ..,
    iSup_mono fun i ↦ sup_comm (f i) _ ▸ symmDiff_comm (f i) _ ▸ le_symmDiff_sup_right ..⟩

Suprema Symmetric Difference Inequality: $\left(\bigsqcup_i f_i\right) \mathbin{∆} \left(\bigsqcup_i g_i\right) \leq \bigsqcup_i (f_i \mathbin{∆} g_i)$

Informal description

For any indexed families of elements $(f_i)_{i \in \iota}$ and $(g_i)_{i \in \iota}$ in a complete Boolean algebra $\alpha$, the symmetric difference of their suprema is bounded above by the supremum of their symmetric differences: \[ \left(\bigsqcup_{i} f_i\right) \mathbin{∆} \left(\bigsqcup_{i} g_i\right) \leq \bigsqcup_{i} (f_i \mathbin{∆} g_i). \]

biSup_symmDiff_biSup_le theorem

 {p : ι → Prop} {f g : (i : ι) → p i → α} :
  (⨆ i, ⨆ (h : p i), f i h) ∆ (⨆ i, ⨆ (h : p i), g i h) ≤ ⨆ i, ⨆ (h : p i), ((f i h) ∆ (g i h))

Full source

/-- A `biSup` version of `iSup_symmDiff_iSup_le`. -/
theorem biSup_symmDiff_biSup_le {p : ι → Prop} {f g : (i : ι) → p i → α} :
    (⨆ i, ⨆ (h : p i), f i h) ∆ (⨆ i, ⨆ (h : p i), g i h) ≤
    ⨆ i, ⨆ (h : p i), ((f i h) ∆ (g i h)) :=
  le_trans iSup_symmDiff_iSup_le <|iSup_mono fun _ ↦ iSup_symmDiff_iSup_le

Double Suprema Symmetric Difference Inequality: $\left(\bigsqcup_i \bigsqcup_{h : p_i} f_i h\right) \mathbin{∆} \left(\bigsqcup_i \bigsqcup_{h : p_i} g_i h\right) \leq \bigsqcup_i \bigsqcup_{h : p_i} (f_i h \mathbin{∆} g_i h)$

Informal description

For any indexed family of elements $(f_i)_{i \in \iota}$ and $(g_i)_{i \in \iota}$ in a complete Boolean algebra $\alpha$, where each $f_i$ and $g_i$ is defined for indices satisfying a predicate $p_i$, the symmetric difference of their double suprema is bounded above by the double supremum of their symmetric differences: \[ \left(\bigsqcup_{i} \bigsqcup_{h : p_i} f_i h\right) \mathbin{∆} \left(\bigsqcup_{i} \bigsqcup_{h : p_i} g_i h\right) \leq \bigsqcup_{i} \bigsqcup_{h : p_i} (f_i h \mathbin{∆} g_i h). \]

CompleteAtomicBooleanAlgebra structure

(α : Type u) extends CompleteLattice α, BooleanAlgebra α

Full source

/--
A complete atomic Boolean algebra is a complete Boolean algebra
that is also completely distributive.

We take iSup_iInf_eq as the definition here,
and prove later on that this implies atomicity.
-/
-- We do not directly extend `CompletelyDistribLattice` to avoid having the `hnot` field
-- We do not directly extend `CompleteBooleanAlgebra` to avoid having the `inf_sSup_le_iSup_inf` and
-- `iInf_sup_le_sup_sInf` fields
class CompleteAtomicBooleanAlgebra (α : Type u) extends CompleteLattice α, BooleanAlgebra α where
  protected iInf_iSup_eq {ι : Type u} {κ : ι → Type u} (f : ∀ a, κ a → α) :
    (⨅ a, ⨆ b, f a b) = ⨆ g : ∀ a, κ a, ⨅ a, f a (g a)

Complete atomic Boolean algebra

Informal description

A complete atomic Boolean algebra is a complete lattice $\alpha$ that is also a Boolean algebra and satisfies the completely distributive property, meaning that infinite meets distribute over infinite joins in the lattice.

CompleteAtomicBooleanAlgebra.toCompletelyDistribLattice instance

[CompleteAtomicBooleanAlgebra α] : CompletelyDistribLattice α

Full source

instance (priority := 100) CompleteAtomicBooleanAlgebra.toCompletelyDistribLattice
    [CompleteAtomicBooleanAlgebra α] : CompletelyDistribLattice α where
  __ := ‹CompleteAtomicBooleanAlgebra α›
  __ := BooleanAlgebra.toBiheytingAlgebra

Complete Atomic Boolean Algebras are Completely Distributive Lattices

Informal description

Every complete atomic Boolean algebra is a completely distributive lattice.

CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instance

[CompleteAtomicBooleanAlgebra α] : CompleteBooleanAlgebra α

Full source

instance (priority := 100) CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra
    [CompleteAtomicBooleanAlgebra α] : CompleteBooleanAlgebra α where
  __ := CompletelyDistribLattice.toCompleteDistribLattice
  __ := ‹CompleteAtomicBooleanAlgebra α›
  inf_sSup_le_iSup_inf _ _ := inf_sSup_eq.le
  iInf_sup_le_sup_sInf _ _ := sup_sInf_eq.ge

Complete Atomic Boolean Algebras are Complete Boolean Algebras

Informal description

Every complete atomic Boolean algebra is a complete Boolean algebra.

Prod.instCompleteAtomicBooleanAlgebra instance

[CompleteAtomicBooleanAlgebra α] [CompleteAtomicBooleanAlgebra β] : CompleteAtomicBooleanAlgebra (α × β)

Full source

instance Prod.instCompleteAtomicBooleanAlgebra [CompleteAtomicBooleanAlgebra α]
    [CompleteAtomicBooleanAlgebra β] : CompleteAtomicBooleanAlgebra (α × β) where
  __ := instBooleanAlgebra
  __ := instCompletelyDistribLattice

Componentwise Complete Atomic Boolean Algebra Structure on Products

Informal description

For any two complete atomic Boolean algebras $\alpha$ and $\beta$, the product $\alpha \times \beta$ is also a complete atomic Boolean algebra, with all operations defined componentwise.

Pi.instCompleteAtomicBooleanAlgebra instance

 {ι : Type*} {π : ι → Type*} [∀ i, CompleteAtomicBooleanAlgebra (π i)] : CompleteAtomicBooleanAlgebra (∀ i, π i)

Full source

instance Pi.instCompleteAtomicBooleanAlgebra {ι : Type*} {π : ι → Type*}
    [∀ i, CompleteAtomicBooleanAlgebra (π i)] : CompleteAtomicBooleanAlgebra (∀ i, π i) where
  __ := Pi.instCompleteBooleanAlgebra
  iInf_iSup_eq f := by ext; rw [iInf_iSup_eq]

Pointwise Complete Atomic Boolean Algebra Structure on Product Types

Informal description

For any family of types $(\pi_i)_{i \in \iota}$ where each $\pi_i$ is a complete atomic Boolean algebra, the product type $\prod_{i \in \iota} \pi_i$ is also a complete atomic Boolean algebra, with all operations (meet $\sqcap$, join $\sqcup$, complement $(\cdot)^\complement$, set difference $\setminus$, Heyting implication $\Rightarrow$, top $\top$, and bottom $\bot$) defined pointwise. Specifically: 1. $(f \sqcap g)(i) = f(i) \sqcap g(i)$, 2. $(f \sqcup g)(i) = f(i) \sqcup g(i)$, 3. $f^\complement(i) = (f(i))^\complement$, 4. $(f \setminus g)(i) = f(i) \setminus g(i)$, 5. $(f \Rightarrow g)(i) = f(i) \Rightarrow g(i)$, 6. $\top(i) = \top$, 7. $\bot(i) = \bot$, for all $i \in \iota$ and $f, g \in \prod_{i \in \iota} \pi_i$.

OrderDual.instCompleteAtomicBooleanAlgebra instance

[CompleteAtomicBooleanAlgebra α] : CompleteAtomicBooleanAlgebra αᵒᵈ

Full source

instance OrderDual.instCompleteAtomicBooleanAlgebra [CompleteAtomicBooleanAlgebra α] :
    CompleteAtomicBooleanAlgebra αᵒᵈ where
  __ := instCompleteBooleanAlgebra
  __ := instCompletelyDistribLattice

Order Dual of a Complete Atomic Boolean Algebra is Complete Atomic Boolean

Informal description

For any complete atomic Boolean algebra $\alpha$, the order dual $\alpha^{\text{op}}$ is also a complete atomic Boolean algebra. In this dual structure, the meet and join operations are swapped, and the complement operation remains unchanged.

Prop.instCompleteAtomicBooleanAlgebra instance

: CompleteAtomicBooleanAlgebra Prop

Full source

instance Prop.instCompleteAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra Prop where
  __ := Prop.instCompleteLattice
  __ := Prop.instBooleanAlgebra
  iInf_iSup_eq f := by simp [Classical.skolem]

Complete Atomic Boolean Algebra Structure on Propositions

Informal description

The set of propositions forms a complete atomic Boolean algebra, where: - The meet operation $\sqcap$ corresponds to logical conjunction (and) - The join operation $\sqcup$ corresponds to logical disjunction (or) - The complement operation $(\cdot)^\complement$ corresponds to logical negation - The top element $\top$ corresponds to true - The bottom element $\bot$ corresponds to false - Infinite meets and joins satisfy the completely distributive property This structure models classical propositional logic with complete distributivity.

Prop.instCompleteBooleanAlgebra instance

: CompleteBooleanAlgebra Prop

Full source

instance Prop.instCompleteBooleanAlgebra : CompleteBooleanAlgebra Prop := inferInstance

Complete Boolean Algebra Structure on Propositions

Informal description

The set of propositions forms a complete Boolean algebra, where: - The meet operation $\sqcap$ corresponds to logical conjunction (and) - The join operation $\sqcup$ corresponds to logical disjunction (or) - The complement operation $(\cdot)^\complement$ corresponds to logical negation - The top element $\top$ corresponds to true - The bottom element $\bot$ corresponds to false - Finite meets distribute over arbitrary joins and finite joins distribute over arbitrary meets. This structure models classical propositional logic with complete distributivity.

Function.Injective.frameMinimalAxioms abbrev

 [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] (minAx : Frame.MinimalAxioms β) (f : α → β) (hf : Injective f)
  (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
  (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤)
  (map_bot : f ⊥ = ⊥) : Frame.MinimalAxioms α

Full source

/-- Pullback an `Order.Frame.MinimalAxioms` along an injection. -/
protected abbrev Function.Injective.frameMinimalAxioms [Max α] [Min α] [SupSet α] [InfSet α] [Top α]
    [Bot α] (minAx : Frame.MinimalAxioms β) (f : α → β) (hf : Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a)
    (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : Frame.MinimalAxioms α where
  __ := hf.completeLattice f map_sup map_inf map_sSup map_sInf map_top map_bot
  inf_sSup_le_iSup_inf a s := by
    change f (a ⊓ sSup s) ≤ f _
    rw [← sSup_image, map_inf, map_sSup s, minAx.inf_iSup₂_eq]
    simp_rw [← map_inf]
    exact ((map_sSup _).trans iSup_image).ge

Inheritance of Frame Minimal Axioms via Injective Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types equipped with maximum and minimum operations, supremum and infimum structures, and top and bottom elements. Given a frame structure `minAx` on $\beta$ and an injective function $f : \alpha \to \beta$ that preserves: - suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$, - infima: $f(a \sqcap b) = f(a) \sqcap f(b)$, - arbitrary suprema: $f(\bigsqcup s) = \bigsqcup_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - arbitrary infima: $f(\bigsqcap s) = \bigsqcap_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - top and bottom elements: $f(\top) = \top$ and $f(\bot) = \bot$, then $\alpha$ inherits the frame structure from $\beta$ via $f$.

Function.Injective.coframeMinimalAxioms abbrev

 [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] (minAx : Coframe.MinimalAxioms β) (f : α → β) (hf : Injective f)
  (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
  (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤)
  (map_bot : f ⊥ = ⊥) : Coframe.MinimalAxioms α

Full source

/-- Pullback an `Order.Coframe.MinimalAxioms` along an injection. -/
protected abbrev Function.Injective.coframeMinimalAxioms [Max α] [Min α] [SupSet α] [InfSet α]
    [Top α] [Bot α] (minAx : Coframe.MinimalAxioms β) (f : α → β) (hf : Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a)
    (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : Coframe.MinimalAxioms α where
  __ := hf.completeLattice f map_sup map_inf map_sSup map_sInf map_top map_bot
  iInf_sup_le_sup_sInf a s := by
    change f _ ≤ f (a ⊔ sInf s)
    rw [← sInf_image, map_sup, map_sInf s, minAx.sup_iInf₂_eq]
    simp_rw [← map_sup]
    exact ((map_sInf _).trans iInf_image).le

Inheritance of Coframe Minimal Axioms via Injective Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types equipped with maximum and minimum operations, supremum and infimum structures, and top and bottom elements. Given a coframe structure `minAx` on $\beta$ and an injective function $f : \alpha \to \beta$ that preserves: - suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$, - infima: $f(a \sqcap b) = f(a) \sqcap f(b)$, - arbitrary suprema: $f(\bigsqcup s) = \bigsqcup_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - arbitrary infima: $f(\bigsqcap s) = \bigsqcap_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - top and bottom elements: $f(\top) = \top$ and $f(\bot) = \bot$, then $\alpha$ inherits the coframe structure from $\beta$ via $f$.

Function.Injective.frame abbrev

 [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [Frame β] (f : α → β) (hf : Injective f)
  (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
  (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤)
  (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) : Frame α

Full source

/-- Pullback an `Order.Frame` along an injection. -/
protected abbrev Function.Injective.frame [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α]
    [HasCompl α] [HImp α] [Frame β] (f : α → β) (hf : Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a)
    (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ)
    (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) : Frame α where
  __ := hf.frameMinimalAxioms .of f map_sup map_inf map_sSup map_sInf map_top map_bot
  __ := hf.heytingAlgebra f map_sup map_inf map_top map_bot map_compl map_himp

Frame Structure via Injective Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types equipped with maximum and minimum operations, supremum and infimum structures, top and bottom elements, complement and Heyting implication operations. Given a frame structure on $\beta$ and an injective function $f \colon \alpha \to \beta$ that preserves: - suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - arbitrary suprema: $f(\bigsqcup s) = \bigsqcup_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - arbitrary infima: $f(\bigsqcap s) = \bigsqcap_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - top and bottom elements: $f(\top) = \top$ and $f(\bot) = \bot$, - complements: $f(a^c) = (f(a))^c$ for all $a \in \alpha$, - Heyting implications: $f(a \Rightarrow b) = f(a) \Rightarrow f(b)$ for all $a, b \in \alpha$, then $\alpha$ inherits a frame structure from $\beta$ via $f$.

Function.Injective.coframe abbrev

 [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HNot α] [SDiff α] [Coframe β] (f : α → β) (hf : Injective f)
  (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
  (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤)
  (map_bot : f ⊥ = ⊥) (map_hnot : ∀ a, f (￢a) = ￢f a) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : Coframe α

Full source

/-- Pullback an `Order.Coframe` along an injection. -/
protected abbrev Function.Injective.coframe [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α]
    [HNot α] [SDiff α] [Coframe β] (f : α → β) (hf : Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a)
    (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_hnot : ∀ a, f (￢a) = ￢f a)
    (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : Coframe α where
  __ := hf.coframeMinimalAxioms .of f map_sup map_inf map_sSup map_sInf map_top map_bot
  __ := hf.coheytingAlgebra f map_sup map_inf map_top map_bot map_hnot map_sdiff

Pullback of Coframe Structure Along an Injective Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types equipped with maximum and minimum operations, supremum and infimum structures, top and bottom elements, Heyting negation, and a difference operation. Suppose $\beta$ is a coframe. Given an injective function $f : \alpha \to \beta$ that preserves: - suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - arbitrary suprema: $f(\bigsqcup s) = \bigsqcup_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - arbitrary infima: $f(\bigsqcap s) = \bigsqcap_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - top and bottom elements: $f(\top) = \top$ and $f(\bot) = \bot$, - Heyting negation: $f(\neg a) = \neg f(a)$ for all $a \in \alpha$, - difference operation: $f(a \setminus b) = f(a) \setminus f(b)$ for all $a, b \in \alpha$, then $\alpha$ inherits a coframe structure from $\beta$ via $f$.

Function.Injective.completeDistribLatticeMinimalAxioms abbrev

 [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] (minAx : CompleteDistribLattice.MinimalAxioms β) (f : α → β)
  (hf : Injective f)
  (map_sup :
    let _ := minAx.toCompleteLattice
    ∀ a b, f (a ⊔ b) = f a ⊔ f b)
  (map_inf :
    let _ := minAx.toCompleteLattice
    ∀ a b, f (a ⊓ b) = f a ⊓ f b)
  (map_sSup :
    let _ := minAx.toCompleteLattice
    ∀ s, f (sSup s) = ⨆ a ∈ s, f a)
  (map_sInf :
    let _ := minAx.toCompleteLattice
    ∀ s, f (sInf s) = ⨅ a ∈ s, f a)
  (map_top :
    let _ := minAx.toCompleteLattice
    f ⊤ = ⊤)
  (map_bot :
    let _ := minAx.toCompleteLattice
    f ⊥ = ⊥) :
  CompleteDistribLattice.MinimalAxioms α

Full source

/-- Pullback a `CompleteDistribLattice.MinimalAxioms` along an injection. -/
protected abbrev Function.Injective.completeDistribLatticeMinimalAxioms [Max α] [Min α] [SupSet α]
    [InfSet α] [Top α] [Bot α] (minAx : CompleteDistribLattice.MinimalAxioms β) (f : α → β)
    (hf : Injective f) (map_sup : let _ := minAx.toCompleteLattice
      ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : let _ := minAx.toCompleteLattice
      ∀ a b, f (a ⊓ b) = f a ⊓ f b) (map_sSup : let _ := minAx.toCompleteLattice
      ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : let _ := minAx.toCompleteLattice
      ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : let _ := minAx.toCompleteLattice
      f ⊤ = ⊤) (map_bot : let _ := minAx.toCompleteLattice
      f ⊥ = ⊥) :
    CompleteDistribLattice.MinimalAxioms α where
  __ := hf.frameMinimalAxioms minAx.toFrame f map_sup map_inf map_sSup map_sInf map_top map_bot
  __ := hf.coframeMinimalAxioms minAx.toCoframe f map_sup map_inf map_sSup map_sInf map_top map_bot

Inheritance of Complete Distributive Lattice Minimal Axioms via Injective Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types equipped with maximum and minimum operations, supremum and infimum structures, and top and bottom elements. Given a complete distributive lattice structure `minAx` on $\beta$ and an injective function $f : \alpha \to \beta$ that preserves: - suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - arbitrary suprema: $f(\bigsqcup s) = \bigsqcup_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - arbitrary infima: $f(\bigsqcap s) = \bigsqcap_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - top and bottom elements: $f(\top) = \top$ and $f(\bot) = \bot$, then $\alpha$ inherits the complete distributive lattice structure from $\beta$ via $f$.

Function.Injective.completeDistribLattice abbrev

 [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [HNot α] [SDiff α]
  [CompleteDistribLattice β] (f : α → β) (hf : Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b)
  (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a)
  (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ)
  (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) (map_hnot : ∀ a, f (￢a) = ￢f a) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
  CompleteDistribLattice α

Full source

/-- Pullback a `CompleteDistribLattice` along an injection. -/
protected abbrev Function.Injective.completeDistribLattice [Max α] [Min α] [SupSet α] [InfSet α]
    [Top α] [Bot α] [HasCompl α] [HImp α] [HNot α] [SDiff α] [CompleteDistribLattice β] (f : α → β)
    (hf : Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a)
    (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥)
    (map_compl : ∀ a, f aᶜ = (f a)ᶜ) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b)
    (map_hnot : ∀ a, f (￢a) = ￢f a) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
    CompleteDistribLattice α where
  __ := hf.frame f map_sup map_inf map_sSup map_sInf map_top map_bot map_compl map_himp
  __ := hf.coframe f map_sup map_inf map_sSup map_sInf map_top map_bot map_hnot map_sdiff

Pullback of Complete Distributive Lattice Structure via Injective Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types equipped with maximum and minimum operations, supremum and infimum structures, top and bottom elements, complement, Heyting implication, Heyting negation, and difference operations. Suppose $\beta$ is a complete distributive lattice. Given an injective function $f \colon \alpha \to \beta$ that preserves: - suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - arbitrary suprema: $f(\bigsqcup s) = \bigsqcup_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - arbitrary infima: $f(\bigsqcap s) = \bigsqcap_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - top and bottom elements: $f(\top) = \top$ and $f(\bot) = \bot$, - complements: $f(a^c) = (f(a))^c$ for all $a \in \alpha$, - Heyting implications: $f(a \Rightarrow b) = f(a) \Rightarrow f(b)$ for all $a, b \in \alpha$, - Heyting negations: $f(\neg a) = \neg f(a)$ for all $a \in \alpha$, - differences: $f(a \setminus b) = f(a) \setminus f(b)$ for all $a, b \in \alpha$, then $\alpha$ inherits a complete distributive lattice structure from $\beta$ via $f$.

Function.Injective.completelyDistribLatticeMinimalAxioms abbrev

 [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] (minAx : CompletelyDistribLattice.MinimalAxioms β) (f : α → β)
  (hf : Injective f)
  (map_sup :
    let _ := minAx.toCompleteLattice
    ∀ a b, f (a ⊔ b) = f a ⊔ f b)
  (map_inf :
    let _ := minAx.toCompleteLattice
    ∀ a b, f (a ⊓ b) = f a ⊓ f b)
  (map_sSup :
    let _ := minAx.toCompleteLattice
    ∀ s, f (sSup s) = ⨆ a ∈ s, f a)
  (map_sInf :
    let _ := minAx.toCompleteLattice
    ∀ s, f (sInf s) = ⨅ a ∈ s, f a)
  (map_top :
    let _ := minAx.toCompleteLattice
    f ⊤ = ⊤)
  (map_bot :
    let _ := minAx.toCompleteLattice
    f ⊥ = ⊥) :
  CompletelyDistribLattice.MinimalAxioms α

Full source

/-- Pullback a `CompletelyDistribLattice.MinimalAxioms` along an injection. -/
protected abbrev Function.Injective.completelyDistribLatticeMinimalAxioms [Max α] [Min α] [SupSet α]
    [InfSet α] [Top α] [Bot α] (minAx : CompletelyDistribLattice.MinimalAxioms β) (f : α → β)
    (hf : Injective f) (map_sup : let _ := minAx.toCompleteLattice
      ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : let _ := minAx.toCompleteLattice
      ∀ a b, f (a ⊓ b) = f a ⊓ f b) (map_sSup : let _ := minAx.toCompleteLattice
      ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : let _ := minAx.toCompleteLattice
      ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : let _ := minAx.toCompleteLattice
      f ⊤ = ⊤) (map_bot : let _ := minAx.toCompleteLattice
      f ⊥ = ⊥) :
    CompletelyDistribLattice.MinimalAxioms α where
  __ := hf.completeDistribLatticeMinimalAxioms minAx.toCompleteDistribLattice f map_sup map_inf
    map_sSup map_sInf map_top map_bot
  iInf_iSup_eq g := hf <| by
    simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      minAx.iInf_iSup_eq']

Inheritance of Completely Distributive Lattice Minimal Axioms via Injective Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types equipped with maximum and minimum operations, supremum and infimum structures, and top and bottom elements. Given a completely distributive lattice structure `minAx` on $\beta$ and an injective function $f \colon \alpha \to \beta$ that preserves: - suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - arbitrary suprema: $f(\bigsqcup s) = \bigsqcup_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - arbitrary infima: $f(\bigsqcap s) = \bigsqcap_{a \in s} f(a)$ for any set $s \subseteq \alpha$, - top and bottom elements: $f(\top) = \top$ and $f(\bot) = \bot$, then $\alpha$ inherits the completely distributive lattice structure from $\beta$ via $f$.

Function.Injective.completelyDistribLattice abbrev

 [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [HNot α] [SDiff α]
  [CompletelyDistribLattice β] (f : α → β) (hf : Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b)
  (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a)
  (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ)
  (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) (map_hnot : ∀ a, f (￢a) = ￢f a) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
  CompletelyDistribLattice α

Full source

/-- Pullback a `CompletelyDistribLattice` along an injection. -/
protected abbrev Function.Injective.completelyDistribLattice [Max α] [Min α] [SupSet α] [InfSet α]
    [Top α] [Bot α] [HasCompl α] [HImp α] [HNot α] [SDiff α] [CompletelyDistribLattice β]
    (f : α → β) (hf : Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a)
    (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥)
    (map_compl : ∀ a, f aᶜ = (f a)ᶜ) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b)
    (map_hnot : ∀ a, f (￢a) = ￢f a) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
    CompletelyDistribLattice α where
  __ := hf.completeLattice f map_sup map_inf map_sSup map_sInf map_top map_bot
  __ := hf.biheytingAlgebra f map_sup map_inf map_top map_bot map_compl map_hnot map_himp map_sdiff
  iInf_iSup_eq g := hf <| by
    simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      iInf_iSup_eq]

Pullback of Completely Distributive Lattice Structure Along an Injective Function

Informal description

Let $\alpha$ and $\beta$ be types with lattice structures, where $\beta$ is a completely distributive lattice. Given an injective function $f \colon \alpha \to \beta$ that preserves: - Suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - Infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - Arbitrary suprema: $f(\bigsqcup s) = \bigsqcup_{a \in s} f(a)$ for all $s \subseteq \alpha$, - Arbitrary infima: $f(\bigsqcap s) = \bigsqcap_{a \in s} f(a)$ for all $s \subseteq \alpha$, - Top element: $f(\top) = \top$, - Bottom element: $f(\bot) = \bot$, - Complement: $f(a^c) = (f(a))^c$ for all $a \in \alpha$, - Heyting implication: $f(a \Rightarrow b) = f(a) \Rightarrow f(b)$ for all $a, b \in \alpha$, - Negation: $f(\neg a) = \neg f(a)$ for all $a \in \alpha$, - Difference operation: $f(a \setminus b) = f(a) \setminus f(b)$ for all $a, b \in \alpha$, then $\alpha$ inherits a completely distributive lattice structure from $\beta$ via $f$.

Function.Injective.completeBooleanAlgebra abbrev

 [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [SDiff α] [CompleteBooleanAlgebra β]
  (f : α → β) (hf : Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
  (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤)
  (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b)
  (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : CompleteBooleanAlgebra α

Full source

/-- Pullback a `CompleteBooleanAlgebra` along an injection. -/
protected abbrev Function.Injective.completeBooleanAlgebra [Max α] [Min α] [SupSet α] [InfSet α]
    [Top α] [Bot α] [HasCompl α] [HImp α] [SDiff α] [CompleteBooleanAlgebra β] (f : α → β)
    (hf : Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b)
    (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a)
    (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥)
    (map_compl : ∀ a, f aᶜ = (f a)ᶜ) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b)
    (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
    CompleteBooleanAlgebra α where
  __ := hf.completeLattice f map_sup map_inf map_sSup map_sInf map_top map_bot
  __ := hf.booleanAlgebra f map_sup map_inf map_top map_bot map_compl map_sdiff map_himp
  inf_sSup_le_iSup_inf a s := by
    change f (a ⊓ sSup s) ≤ f _
    rw [← sSup_image, map_inf, map_sSup s, inf_iSup₂_eq]
    simp_rw [← map_inf]
    exact ((map_sSup _).trans iSup_image).ge
  iInf_sup_le_sup_sInf a s := by
    change f _ ≤ f (a ⊔ sInf s)
    rw [← sInf_image, map_sup, map_sInf s, sup_iInf₂_eq]
    simp_rw [← map_sup]
    exact ((map_sInf _).trans iInf_image).le

Pullback of Complete Boolean Algebra Structure via Injective Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types equipped with lattice structures, where $\beta$ is a complete Boolean algebra. Given an injective function $f \colon \alpha \to \beta$ that preserves: - Suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - Infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - Arbitrary suprema: $f(\bigsqcup s) = \bigsqcup_{a \in s} f(a)$ for all $s \subseteq \alpha$, - Arbitrary infima: $f(\bigsqcap s) = \bigsqcap_{a \in s} f(a)$ for all $s \subseteq \alpha$, - Top element: $f(\top) = \top$, - Bottom element: $f(\bot) = \bot$, - Complement: $f(a^\complement) = (f(a))^\complement$ for all $a \in \alpha$, - Heyting implication: $f(a \Rightarrow b) = f(a) \Rightarrow f(b)$ for all $a, b \in \alpha$, - Relative complement: $f(a \setminus b) = f(a) \setminus f(b)$ for all $a, b \in \alpha$, then $\alpha$ inherits a complete Boolean algebra structure from $\beta$ via $f$.

Function.Injective.completeAtomicBooleanAlgebra abbrev

 [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [HNot α] [SDiff α]
  [CompleteAtomicBooleanAlgebra β] (f : α → β) (hf : Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b)
  (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a)
  (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ)
  (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) (map_hnot : ∀ a, f (￢a) = ￢f a) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
  CompleteAtomicBooleanAlgebra α

Full source

/-- Pullback a `CompleteAtomicBooleanAlgebra` along an injection. -/
protected abbrev Function.Injective.completeAtomicBooleanAlgebra [Max α] [Min α] [SupSet α]
    [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [HNot α] [SDiff α]
    [CompleteAtomicBooleanAlgebra β] (f : α → β) (hf : Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a)
    (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥)
    (map_compl : ∀ a, f aᶜ = (f a)ᶜ) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b)
    (map_hnot : ∀ a, f (￢a) = ￢f a) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
    CompleteAtomicBooleanAlgebra α where
  __ := hf.completelyDistribLattice f map_sup map_inf map_sSup map_sInf map_top map_bot map_compl
    map_himp map_hnot map_sdiff
  __ := hf.booleanAlgebra f map_sup map_inf map_top map_bot map_compl map_sdiff map_himp

Pullback of Complete Atomic Boolean Algebra Structure Along an Injective Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types with lattice structures, where $\beta$ is a complete atomic Boolean algebra. Given an injective function $f \colon \alpha \to \beta$ that preserves: - Suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - Infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - Arbitrary suprema: $f(\bigsqcup s) = \bigsqcup_{a \in s} f(a)$ for all $s \subseteq \alpha$, - Arbitrary infima: $f(\bigsqcap s) = \bigsqcap_{a \in s} f(a)$ for all $s \subseteq \alpha$, - Top element: $f(\top) = \top$, - Bottom element: $f(\bot) = \bot$, - Complement: $f(a^\complement) = (f(a))^\complement$ for all $a \in \alpha$, - Heyting implication: $f(a \Rightarrow b) = f(a) \Rightarrow f(b)$ for all $a, b \in \alpha$, - Negation: $f(\neg a) = \neg f(a)$ for all $a \in \alpha$, - Difference operation: $f(a \setminus b) = f(a) \setminus f(b)$ for all $a, b \in \alpha$, then $\alpha$ inherits a complete atomic Boolean algebra structure from $\beta$ via $f$.

PUnit.instCompleteAtomicBooleanAlgebra instance

: CompleteAtomicBooleanAlgebra PUnit

Full source

instance instCompleteAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra PUnit where
  __ := PUnit.instBooleanAlgebra
  sSup _ := unit
  sInf _ := unit
  le_sSup _ _ _ := trivial
  sSup_le _ _ _ := trivial
  sInf_le _ _ _ := trivial
  le_sInf _ _ _ := trivial
  iInf_iSup_eq _ := rfl

Complete Atomic Boolean Algebra Structure on the Trivial Type

Informal description

The trivial type `PUnit` (the type with a single element) has a canonical complete atomic Boolean algebra structure, where all operations (meet, join, complement, set difference, and Heyting implication) are defined in the trivial way.

PUnit.instCompleteBooleanAlgebra instance

: CompleteBooleanAlgebra PUnit

Full source

instance instCompleteBooleanAlgebra : CompleteBooleanAlgebra PUnit := inferInstance

Complete Boolean Algebra Structure on the Trivial Type

Informal description

The trivial type `PUnit` (the type with a single element) has a canonical complete Boolean algebra structure, where all operations (meet, join, complement, set difference, and Heyting implication) are defined in the trivial way.

PUnit.sSup_eq theorem

: sSup s = unit

Full source

@[simp]
theorem sSup_eq : sSup s = unit :=
  rfl

Supremum in Trivial Type Equals Unit Element

Informal description

For any set $s$ of elements in the trivial type `PUnit`, the supremum (least upper bound) of $s$ is equal to the unique element `unit` of `PUnit`.

PUnit.sInf_eq theorem

: sInf s = unit

Full source

@[simp]
theorem sInf_eq : sInf s = unit :=
  rfl

Infimum in Trivial Type is Unit

Informal description

For any subset $s$ of the trivial type `PUnit`, the infimum of $s$ is equal to the unique element `unit` of `PUnit`.

Mathlib.Order.CompleteBooleanAlgebra

Typeclasses

References