le_map — Mathlib

English

If a function h sends every set s in f to an image m''s in g, then g ≤ map m f.

Русский

Если для каждого множества s ∈ f образ m(s) ∈ g, то g ≤ map m f.

LaTeX

$$le_map {f : Filter α} {m : α → β} {g : Filter β} (h : ∀ s ∈ f, m '' s ∈ g) : g ≤ f.map m$$

Lean4

theorem le_map {f : Filter α} {m : α → β} {g : Filter β} (h : ∀ s ∈ f, m '' s ∈ g) : g ≤ f.map m := fun _ hs =>
  mem_of_superset (h _ hs) <| image_preimage_subset _ _

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