lift'_iInf — Mathlib

English

Let ι be nonempty and f : ι → Filter α, g : Set α → Set β with hg(s,t) = g(s ∩ t) = g(s) ∩ g(t). Then (iInf f).lift' g = ⨅ i, (f i).lift' g.

Русский

Пусть индексный набор непуст и есть путь f: ι → Filter α, g: Set α → Set β, такое что hg(s,t) = g(s ∩ t) = g(s) ∩ g(t). Тогда (iInf f).lift' g = ⨅ i, (f i).lift' g.

LaTeX

$$$(iInf f).lift' g = \\bigwedge_i (f(i).lift' g)$$$

Lean4

theorem lift'_iInf [Nonempty ι] {f : ι → Filter α} {g : Set α → Set β} (hg : ∀ s t, g (s ∩ t) = g s ∩ g t) :
    (iInf f).lift' g = ⨅ i, (f i).lift' g :=
  lift_iInf fun s t => by simp only [inf_principal, comp, hg]

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