l_biInf_of_ul_eq_self — Mathlib

English

Under gi, if f : ∀ i (p i) → α and hf : ∀ i hi, u(l(f(i, hi))) = f(i, hi), then l( inf_i hi f(i, hi) ) = inf_i hi l( f(i, hi) ).

Русский

Пусть gi — связь Галуа; если дано f(i, hi) ∈ α и hf: u(l(f(i, hi))) = f(i, hi) для всех i, hi, то l( инф_i hi f(i, hi) ) = инф_i hi l( f(i, hi) ).

LaTeX

$$$$ l\left( \bigwedge_{i}(\;\bigwedge_{h i} f(i,h i)\;) \right) = \bigwedge_{i}(\;\bigwedge_{h i} l(f(i,h i))\;). $$$$

Lean4

theorem l_biInf_of_ul_eq_self [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x}
    {p : ι → Prop} (f : ∀ (i) (_ : p i), α) (hf : ∀ i hi, u (l (f i hi)) = f i hi) :
    l (⨅ (i) (hi), f i hi) = ⨅ (i) (hi), l (f i hi) :=
  by
  rw [iInf_subtype', iInf_subtype']
  exact gi.l_iInf_of_ul_eq_self _ fun _ => hf _ _

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