le_map_iff — Mathlib

English

An equivalence holds: g ≤ map m f iff every image of s in f under m lies in g.

Русский

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

LaTeX

$$le_map_iff {f : Filter α} {m : α → β} {g : Filter β} : g ≤ f.map m ↔ ∀ s ∈ f, m '' s ∈ g$$

Lean4

theorem le_map_iff {f : Filter α} {m : α → β} {g : Filter β} : g ≤ f.map m ↔ ∀ s ∈ f, m '' s ∈ g :=
  ⟨fun h _ hs => h (image_mem_map hs), le_map⟩

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