toDistribLattice — Mathlib

English

Galois connection holds between x ↦ x \\ a and a ⊔ x in a generalized co-Heyting algebra: for all x,y, x \\ a ≤ y iff x ≤ a ⊔ y.

Русский

Галуа связь между отображениями x ↦ x \\ a и a ⊔ x в обобщённой коейтинговой алгебре: для всех x,y выполняется x \\ a ≤ y ⇔ x ≤ a ⊔ y.

LaTeX

$$$ \\forall x,y \\in \\alpha:\\; x \\setminus a \\le y \\iff x \\le a \\sqcup y $$$

Lean4

instance (priority := 100) toDistribLattice : DistribLattice α :=
  { ‹GeneralizedCoheytingAlgebra α› with
    le_sup_inf := fun a b c => by simp_rw [← sdiff_le_iff, le_inf_iff, sdiff_le_iff, ← le_inf_iff]; rfl }

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