sInter_lift'_sets — Mathlib

English

The intersection of all sets in f.lift' h equals the intersection over s ∈ f of h s.

Русский

Пусть пересечение всех множеств из f.lift' h равно пересечению по s ∈ f из h s.

LaTeX

$$$ \\bigcap_0 \\{s \\mid s \\in f.lift' h\\} = \\bigcap_{s \\in f} h s $$$

Lean4

theorem sInter_lift'_sets (hh : Monotone h) : ⋂₀ {s | s ∈ f.lift' h} = ⋂ s ∈ f, h s :=
  (sInter_lift_sets (monotone_principal.comp hh)).trans <| iInter₂_congr fun _ _ => csInf_Ici

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