English
Let f and g be filters on α, and let m: α → β be such that m is injective on some set s with s ∈ f and s ∈ g. Then the pushforward filters satisfy map m f = map m g if and only if f = g.
Русский
Пусть f и g — фильтры на α, а m: α → β такова, что она инъективна на некотором множестве s, где s ∈ f и s ∈ g. Тогда образующие фильтры по m удовлетворяют map m f = map m g тогда и только тогда, когда f = g.
LaTeX
$$$\operatorname{map} m f = \operatorname{map} m g \iff f = g$$$
Lean4
theorem map_eq_map_iff_of_injOn {f g : Filter α} {m : α → β} {s : Set α} (hsf : s ∈ f) (hsg : s ∈ g) (hm : InjOn m s) :
map m f = map m g ↔ f = g := by
simp only [le_antisymm_iff, map_le_map_iff_of_injOn hsf hsg hm, map_le_map_iff_of_injOn hsg hsf hm]
