gc_sdiff_sup — Mathlib

English

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

Русский

Галуа-связь между отображениями x ↦ x \\ a и y ↦ a ⊔ y в обобщённой коейтинговой алгебре: для всех 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

theorem gc_sdiff_sup : GaloisConnection (· \ a) (a ⊔ ·) := fun _ _ ↦ sdiff_le_iff

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