lift'_iInf_of_map_univ — Mathlib

English

If g preserves intersections and maps univ to univ, then (iInf f).lift' g = ⨅ i, (f i).lift' g.

Русский

Если g сохраняет пересечения и отображает единицу на единицу, то (iInf f).lift' g = ⨅ i, (f i).lift' g.

LaTeX

$$$\\bigl( \\forall s,t,\\; g(s \\cap t) = g(s) \\cap g(t) \\bigr) \\land (g(\\mathrm{univ}) = \\mathrm{univ}) \\Rightarrow (iInf f).lift' g = \\bigwedge_i (f(i).lift' g)$$$

Lean4

theorem lift'_iInf_of_map_univ {f : ι → Filter α} {g : Set α → Set β} (hg : ∀ {s t}, g (s ∩ t) = g s ∩ g t)
    (hg' : g univ = univ) : (iInf f).lift' g = ⨅ i, (f i).lift' g :=
  lift_iInf_of_map_univ (fun s t => by simp only [inf_principal, comp, hg])
    (by rw [Function.comp_apply, hg', principal_univ])

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