map — Mathlib

English

If l has a basis (p, s), then the image filter l.map f has a basis with index i corresponding to the image f''s i.

Русский

Если у l есть базис (p, s), то образующий фильтр l.map f имеет базис с индексом i, соответствующим образу f'' s i.

LaTeX

$$$ (l.map f).HasBasis p (fun i => f'' s i) $$$

Lean4

theorem map (f : α → β) (hl : l.HasBasis p s) : (l.map f).HasBasis p fun i => f '' s i :=
  ⟨fun t => by simp only [mem_map, image_subset_iff, hl.mem_iff, preimage]⟩

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