to_image_id' — Mathlib

English

If l has basis p s, then l has a basis given by the relation t ↦ ∃ i, p i ∧ s i = t, with identity index.

Русский

Если у фильтра есть базис p s, то базисом является отображение t ↦ ∃ i, p i ∧ s i = t с единичным индексом.

LaTeX

$$to_image_id' (h : l.HasBasis p s) : l.HasBasis (fun t => Exists i, p i ∧ s i = t) id$$

Lean4

theorem to_image_id' (h : l.HasBasis p s) : l.HasBasis (fun t ↦ ∃ i, p i ∧ s i = t) id :=
  ⟨fun _ ↦ by simp [h.mem_iff]⟩

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