hasBasis_iInf_of_directed' — Mathlib

English

If l has a basis p s and e is an equivalence, then l has a basis with p ∘ e and s ∘ e.

Русский

Если у базиса фильтра есть эквивалентная перестановка индексов e, то новый базис имеет p ∘ e и s ∘ e.

LaTeX

$$comp_equiv (h : l.HasBasis p s) (e : ι' ≃ ι) : l.HasBasis (p ∘ e) (s ∘ e)$$

Lean4

theorem hasBasis_iInf_of_directed' {ι : Type*} {ι' : ι → Sort _} [Nonempty ι] {l : ι → Filter α} (s : ∀ i, ι' i → Set α)
    (p : ∀ i, ι' i → Prop) (hl : ∀ i, (l i).HasBasis (p i) (s i)) (h : Directed (· ≥ ·) l) :
    (⨅ i, l i).HasBasis (fun ii' : Σ i, ι' i => p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2 :=
  by
  refine ⟨fun t => ?_⟩
  rw [mem_iInf_of_directed h, Sigma.exists]
  exact exists_congr fun i => (hl i).mem_iff

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