comap — Mathlib

English

If h_pi is a π-system of sets in β and f: α → β, then the preimage-collection { s ⊆ α : ∃ t ∈ S, f⁻¹ t = s } is a π-system.

Русский

Если h_pi — π-система множеств в β и f: α → β, тогда множество предварительных образов { s ⊆ α | ∃ t ∈ S, f⁻¹ t = s } образует π-систему.

LaTeX

$$$ IsPiSystem\ {s : Set\ α\;|\;∃ t ∈ S,\ f^{-1}' t = s} $$$

Lean4

theorem comap {α β} {S : Set (Set β)} (h_pi : IsPiSystem S) (f : α → β) :
    IsPiSystem {s : Set α | ∃ t ∈ S, f ⁻¹' t = s} :=
  by
  rintro _ ⟨s, hs_mem, rfl⟩ _ ⟨t, ht_mem, rfl⟩ hst
  rw [← Set.preimage_inter] at hst ⊢
  exact ⟨s ∩ t, h_pi s hs_mem t ht_mem (nonempty_of_nonempty_preimage hst), rfl⟩

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