l_iInf_of_ul_eq_self — Mathlib

English

If gi is a Galois insertion and f: ι → α satisfies u(l(f(i))) = f(i) for all i, then l( inf_i f(i) ) = inf_i l(f(i)).

Русский

Если gi — связь Галуа и для всех i выполняется u(l(f(i))) = f(i), то l( inf_i f(i) ) = inf_i l(f(i)).

LaTeX

$$$$ l\left( \inf_{i} f(i) \right) = \inf_{i} l\big(f(i)\big). $$$$

Lean4

theorem l_iInf_of_ul_eq_self [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} (f : ι → α)
    (hf : ∀ i, u (l (f i)) = f i) : l (⨅ i, f i) = ⨅ i, l (f i) :=
  calc
    l (⨅ i, f i) = l (⨅ i : ι, u (l (f i))) := by simp [hf]
    _ = ⨅ i, l (f i) := gi.l_iInf_u _

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