English
The intersection of the sets of the comapped filter equals the iterated preimage intersection over the filter base.
Русский
Пересечение множеств, образованных через обратный образ фильтра, равно пересечению по предельному основанию фильтра.
LaTeX
$$⋂₀ (comap f F).sets = ⋂ U ∈ F, f ⁻¹' U$$
Lean4
theorem sInter_comap_sets (f : α → β) (F : Filter β) : ⋂₀ (comap f F).sets = ⋂ U ∈ F, f ⁻¹' U :=
by
ext x
suffices (∀ (A : Set α) (B : Set β), B ∈ F → f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B : Set β, B ∈ F → f x ∈ B by
simp only [mem_sInter, mem_iInter, Filter.mem_sets, mem_comap, this, and_imp, mem_preimage, exists_imp]
constructor
· intro h U U_in
simpa only [Subset.rfl, forall_prop_of_true, mem_preimage] using h (f ⁻¹' U) U U_in
· intro h V U U_in f_U_V
exact f_U_V (h U U_in)
