Mathlib.Order.PropInstances

Prop.instDistribLattice instance

: DistribLattice Prop

Full source

/-- Propositions form a distributive lattice. -/
instance Prop.instDistribLattice : DistribLattice Prop where
  sup := Or
  le_sup_left := @Or.inl
  le_sup_right := @Or.inr
  sup_le := fun _ _ _ => Or.rec
  inf := And
  inf_le_left := @And.left
  inf_le_right := @And.right
  le_inf := fun _ _ _ Hab Hac Ha => And.intro (Hab Ha) (Hac Ha)
  le_sup_inf := fun _ _ _ => or_and_left.2

Propositions Form a Distributive Lattice

Informal description

The set of propositions forms a distributive lattice, where the join operation corresponds to logical OR ($\lor$) and the meet operation corresponds to logical AND ($\land$). This means that for any propositions $P$, $Q$, and $R$, the following distributivity property holds: $$(P \lor Q) \land (P \lor R) \leftrightarrow P \lor (Q \land R).$$

Prop.instBoundedOrder instance

: BoundedOrder Prop

Full source

/-- Propositions form a bounded order. -/
instance Prop.instBoundedOrder : BoundedOrder Prop where
  top := True
  le_top _ _ := True.intro
  bot := False
  bot_le := @False.elim

Propositions Form a Bounded Order

Informal description

The set of propositions forms a bounded order, where the greatest element $\top$ is `True` and the least element $\bot$ is `False`.

Prop.bot_eq_false theorem

: (⊥ : Prop) = False

Full source

@[simp]
theorem Prop.bot_eq_false : (⊥ : Prop) = False :=
  rfl

Bottom Element in Proposition Lattice is False

Informal description

The bottom element in the lattice of propositions is equal to `False`, i.e., $\bot = \text{False}$.

Prop.top_eq_true theorem

: (⊤ : Prop) = True

Full source

@[simp]
theorem Prop.top_eq_true : (⊤ : Prop) = True :=
  rfl

Top Element in Proposition Lattice is True

Informal description

The top element in the lattice of propositions is equal to `True`, i.e., $\top = \text{True}$.

Prop.le_isTotal instance

: IsTotal Prop (· ≤ ·)

Full source

instance Prop.le_isTotal : IsTotal Prop (· ≤ ·) :=
  ⟨fun p q => by by_cases h : q <;> simp [h]⟩

Totality of the Order on Propositions

Informal description

The relation $\leq$ on the lattice of propositions is total, meaning that for any two propositions $P$ and $Q$, either $P \leq Q$ or $Q \leq P$ holds.

Prop.linearOrder instance

: LinearOrder Prop

Full source

noncomputable instance Prop.linearOrder : LinearOrder Prop := by
  classical
  exact Lattice.toLinearOrder Prop

Linear Order Structure on Propositions

Informal description

The set of propositions forms a linear order, where the order relation is given by implication ($\leq$ corresponds to $\rightarrow$), and the join and meet operations correspond to logical OR ($\lor$) and AND ($\land$) respectively.

sup_Prop_eq theorem

: (· ⊔ ·) = (· ∨ ·)

Full source

@[simp]
theorem sup_Prop_eq : (· ⊔ ·) = (· ∨ ·) :=
  rfl

Supremum Equals Logical OR in Proposition Lattice

Informal description

The supremum operation $\sqcup$ on the lattice of propositions coincides with the logical OR operation $\lor$, i.e., for any propositions $P$ and $Q$, $P \sqcup Q = P \lor Q$.

inf_Prop_eq theorem

: (· ⊓ ·) = (· ∧ ·)

Full source

@[simp]
theorem inf_Prop_eq : (· ⊓ ·) = (· ∧ ·) :=
  rfl

Infimum of Propositions is Logical Conjunction

Informal description

The infimum operation on propositions coincides with logical conjunction, i.e., for any propositions $P$ and $Q$, $P \sqcap Q = P \land Q$.

Pi.disjoint_iff theorem

[∀ i, OrderBot (α' i)] {f g : ∀ i, α' i} : Disjoint f g ↔ ∀ i, Disjoint (f i) (g i)

Full source

theorem disjoint_iff [∀ i, OrderBot (α' i)] {f g : ∀ i, α' i} :
    DisjointDisjoint f g ↔ ∀ i, Disjoint (f i) (g i) := by
  classical
  constructor
  · intro h i x hf hg
    exact (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => bot_le⟩)
      (update_le_iff.mpr ⟨hg, fun _ _ => bot_le⟩)).1
  · intro h x hf hg i
    apply h i (hf i) (hg i)

Pointwise Disjointness Criterion in Product of Ordered Types with Bottom Elements

Informal description

For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ is equipped with a partial order and has a least element $\bot$, two functions $f, g : \forall i, \alpha_i$ are disjoint (i.e., $f \sqcap g = \bot$) if and only if for every index $i$, the elements $f(i)$ and $g(i)$ are disjoint in $\alpha_i$.

Pi.codisjoint_iff theorem

[∀ i, OrderTop (α' i)] {f g : ∀ i, α' i} : Codisjoint f g ↔ ∀ i, Codisjoint (f i) (g i)

Full source

theorem codisjoint_iff [∀ i, OrderTop (α' i)] {f g : ∀ i, α' i} :
    CodisjointCodisjoint f g ↔ ∀ i, Codisjoint (f i) (g i) :=
  @disjoint_iff _ (fun i => (α' i)ᵒᵈ) _ _ _ _

Pointwise Codisjointness Criterion in Product of Ordered Types with Top Elements

Informal description

For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ is equipped with a partial order and has a greatest element $\top$, two functions $f, g : \forall i, \alpha_i$ are codisjoint (i.e., $f \sqcup g = \top$) if and only if for every index $i$, the elements $f(i)$ and $g(i)$ are codisjoint in $\alpha_i$.

Pi.isCompl_iff theorem

[∀ i, BoundedOrder (α' i)] {f g : ∀ i, α' i} : IsCompl f g ↔ ∀ i, IsCompl (f i) (g i)

Full source

theorem isCompl_iff [∀ i, BoundedOrder (α' i)] {f g : ∀ i, α' i} :
    IsComplIsCompl f g ↔ ∀ i, IsCompl (f i) (g i) := by
  simp_rw [_root_.isCompl_iff, disjoint_iff, codisjoint_iff, forall_and]

Pointwise Complement Criterion in Product of Bounded Orders

Informal description

For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ is equipped with a bounded order (having both a greatest element $\top$ and a least element $\bot$), two functions $f, g : \forall i, \alpha_i$ are complements (i.e., $f \sqcap g = \bot$ and $f \sqcup g = \top$) if and only if for every index $i$, the elements $f(i)$ and $g(i)$ are complements in $\alpha_i$.

Prop.disjoint_iff theorem

{P Q : Prop} : Disjoint P Q ↔ ¬(P ∧ Q)

Full source

@[simp]
theorem Prop.disjoint_iff {P Q : Prop} : DisjointDisjoint P Q ↔ ¬(P ∧ Q) :=
  disjoint_iff_inf_le

Disjointness Criterion for Propositions: $\text{Disjoint}(P, Q) \leftrightarrow \neg (P \land Q)$

Informal description

For any two propositions $P$ and $Q$, they are disjoint (i.e., their meet is false) if and only if they are not both true simultaneously, i.e., $\text{Disjoint}(P, Q) \leftrightarrow \neg (P \land Q)$.

Prop.codisjoint_iff theorem

{P Q : Prop} : Codisjoint P Q ↔ P ∨ Q

Full source

@[simp]
theorem Prop.codisjoint_iff {P Q : Prop} : CodisjointCodisjoint P Q ↔ P ∨ Q :=
  codisjoint_iff_le_sup.trans <| forall_const True

Codisjointness in Propositions is Equivalent to Logical OR

Informal description

For any two propositions $P$ and $Q$, they are codisjoint (i.e., their join is the greatest element $\top$) if and only if at least one of $P$ or $Q$ is true, i.e., $P \lor Q$ holds.

Prop.isCompl_iff theorem

{P Q : Prop} : IsCompl P Q ↔ ¬(P ↔ Q)

Full source

@[simp]
theorem Prop.isCompl_iff {P Q : Prop} : IsComplIsCompl P Q ↔ ¬(P ↔ Q) := by
  rw [_root_.isCompl_iff, Prop.disjoint_iff, Prop.codisjoint_iff, not_iff]
  by_cases P <;> by_cases Q <;> simp [*]

Complementary Propositions Criterion: $\text{IsCompl}(P, Q) \leftrightarrow \neg (P \leftrightarrow Q)$

Informal description

For any two propositions $P$ and $Q$, they are complements in the lattice of propositions (i.e., $P \sqcap Q = \bot$ and $P \sqcup Q = \top$) if and only if they are not logically equivalent, i.e., $\text{IsCompl}(P, Q) \leftrightarrow \neg (P \leftrightarrow Q)$.

Prop.decidablePredBot instance

: DecidablePred (⊥ : α → Prop)

Full source

instance Prop.decidablePredBot : DecidablePred (⊥ : α → Prop) := fun _ => instDecidableFalse

Decidability of the Constant False Predicate

Informal description

For any type $\alpha$, the constant false predicate $\bot : \alpha \to \text{Prop}$ is decidable.

Prop.decidablePredTop instance

: DecidablePred (⊤ : α → Prop)

Full source

instance Prop.decidablePredTop : DecidablePred (⊤ : α → Prop) := fun _ => instDecidableTrue

Decidability of the Constant True Predicate

Informal description

For any type $\alpha$, the constant true predicate $\top : \alpha \to \text{Prop}$ is decidable.

Prop.decidableRelBot instance

: DecidableRel (⊥ : α → α → Prop)

Full source

instance Prop.decidableRelBot : DecidableRel (⊥ : α → α → Prop) := fun _ _ => instDecidableFalse

Decidability of the Constant False Binary Relation

Informal description

For any type $\alpha$, the constant false binary relation $\bot : \alpha \to \alpha \to \text{Prop}$ is decidable.

Prop.decidableRelTop instance

: DecidableRel (⊤ : α → α → Prop)

Full source

instance Prop.decidableRelTop : DecidableRel (⊤ : α → α → Prop) := fun _ _ => instDecidableTrue

Decidability of the Constant True Binary Relation

Informal description

For any type $\alpha$, the constant true binary relation $\top : \alpha \to \alpha \to \text{Prop}$ is decidable.