inf_eq_iInf — Mathlib

English

Let α be a complete lattice and x,y ∈ α. Then the meet x ∧ y equals the infimum over booleans b of cond(b, x, y): x ∧ y = inf_{b ∈ {true,false}} cond(b, x, y).

Русский

Пусть α — полная решетка и x, y ∈ α. Тогда их пересечение x ∧ y равно инфимину над булевыми значениями: x ∧ y = inf_{b ∈ {true,false}} cond(b, x, y).

LaTeX

$$$x \land y = \inf_{b \in \{true,false\}} \operatorname{cond}(b,x,y)$$$

Lean4

theorem inf_eq_iInf (x y : α) : x ⊓ y = ⨅ b : Bool, cond b x y :=
  @sup_eq_iSup αᵒᵈ _ _ _

Похожие утверждения