English
The inverse map of a filter: for a function m : α → β and a filter f on β, comap m f is the filter on α with sets of the form {s | ∃ t ∈ f, m^{-1}(t) ⊆ s}, together with the usual univ, supersets, and finite intersections properties.
Русский
Обратное отображение фильтра: для отображения m: α → β и фильтра f на β, comap m f задаёт фильтр на α, имеющий множества {s | ∃ t ∈ f, m^{-1}(t) ⊆ s} и удовлетворяющий свойствам фильтра.
LaTeX
$$$\\mathrm{comap}(m,f) :\\; \\text{sets} := \\{s \\mid \\exists t \\in f,\\ m^{-1}(t) \\subseteq s\\}$$$
Lean4
/-- The inverse map of a filter. A set `s` belongs to `Filter.comap m f` if either of the following
equivalent conditions hold.
1. There exists a set `t ∈ f` such that `m ⁻¹' t ⊆ s`. This is used as a definition.
2. The set `kernImage m s = {y | ∀ x, m x = y → x ∈ s}` belongs to `f`, see `Filter.mem_comap'`.
3. The set `(m '' sᶜ)ᶜ` belongs to `f`, see `Filter.mem_comap_iff_compl` and
`Filter.compl_mem_comap`. -/
def comap (m : α → β) (f : Filter β) : Filter α
where
sets := {s | ∃ t ∈ f, m ⁻¹' t ⊆ s}
univ_sets := ⟨univ, univ_mem, subset_univ _⟩
sets_of_superset := fun ⟨a', ha', ma'a⟩ ab => ⟨a', ha', ma'a.trans ab⟩
inter_sets := fun ⟨a', ha₁, ha₂⟩ ⟨b', hb₁, hb₂⟩ => ⟨a' ∩ b', inter_mem ha₁ hb₁, inter_subset_inter ha₂ hb₂⟩
