comap — Mathlib

English

If l has a basis p s, then the comap filter l.comap f has a basis given by preimages of s i.

Русский

Если у l есть базис p s, то фильтр comap l по f имеет базис, заданный через предобразные множества s i.

LaTeX

$$$ (l.comap f).HasBasis p (fun i => f^{-1}'(s i)) $$$

Lean4

theorem comap (f : β → α) (hl : l.HasBasis p s) : (l.comap f).HasBasis p fun i => f ⁻¹' s i :=
  ⟨fun t => by
    simp only [mem_comap', hl.mem_iff]
    refine exists_congr (fun i => Iff.rfl.and ?_)
    exact ⟨fun h x hx => h hx rfl, fun h y hy x hx => h <| by rwa [mem_preimage, hx]⟩⟩

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