English
If P is a complete semilattice inf, principal and Inf form a Galois coinsertion between P and PFilter P.
Русский
Если P — полная полупорядованная пониженная, то principal и Inf образуют коинсерт между P и PFilter P.
LaTeX
$$$$ \\text{infGi} : \\text{GaloisCoinsertion}(x \\mapsto toDual(principal x), F \\mapsto sInf(ofDual F)) $$$$
Lean4
/-- If a poset `P` admits arbitrary `Inf`s, then `principal` and `Inf` form a Galois coinsertion. -/
def infGi : GaloisCoinsertion (fun x => toDual (principal x)) fun F => sInf (ofDual F : PFilter P) :=
sInf_gc.toGaloisCoinsertion fun _ => sInf_le <| mem_principal.2 le_rfl
