sInter_lift_sets — Mathlib

English

The intersection of all sets in f.lift g equals the intersection over s ∈ f of the intersections over t ∈ g s: ⋂₀ {s | s ∈ f.lift g} = ⋂ s ∈ f, ⋂₀ {t | t ∈ g s}.

Русский

Пересечение всех множеств в f.lift g равно пересечению по s ∈ f от пересечений по t ∈ g s: ⋂₀ {s | s ∈ f.lift g} = ⋂ s ∈ f, ⋂₀ {t | t ∈ g s}.

LaTeX

$$$\\bigcap_0 \\{ s \\mid s \\in f.lift g \\} = \\bigcap_{s \\in f} \\bigcap_0 \\{ t \\mid t \\in g\\,s \\}$$$

Lean4

theorem sInter_lift_sets (hg : Monotone g) : ⋂₀ {s | s ∈ f.lift g} = ⋂ s ∈ f, ⋂₀ {t | t ∈ g s} := by
  simp only [sInter_eq_biInter, mem_setOf_eq, mem_lift_sets hg, iInter_exists, iInter_and, @iInter_comm _ (Set β)]

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