sInf_gc — Mathlib

English

There is a Galois connection between principal and Inf when P is a complete semilattice inf.

Русский

При полной полупрорядке Inf существует связь Галуа между функциями principal и Inf.

LaTeX

$$$$ \\text{le}_{\\mathsf{PFilter}}(\\text{toDual}(\\text{principal}(x)), F) \\iff x \\le \\mathrm{sInf}(\\mathrm{ofDual}(F)). $$$$

Lean4

theorem sInf_gc : GaloisConnection (fun x => toDual (principal x)) fun F => sInf (ofDual F : PFilter P) := fun x F => by
  simp only [le_sInf_iff, SetLike.mem_coe, toDual_le, SetLike.le_def, mem_principal]

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