map_inj — Mathlib

English

If m: α → β is injective, then the map m of filters is injective, i.e., map m f = map m g implies f = g for any filters f, g on α.

Русский

Если m: α → β инъективна, то отображение фильтров через m инъективно, т.е. map m f = map m g приводит к f = g для любых фильтров f, g на α.

LaTeX

$$$\text{Injective}(m) \;\Rightarrow\; (\operatorname{map} m f = \operatorname{map} m g \iff f = g)$$$

Lean4

theorem map_inj {f g : Filter α} {m : α → β} (hm : Injective m) : map m f = map m g ↔ f = g :=
  map_eq_map_iff_of_injOn univ_mem univ_mem hm.injOn

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