ge_iff — Mathlib

English

For any filter l, l HasBasis (fun s => s ∈ l) id; the basis is given by its own members.

Русский

Для любого фильтра l имеет место HasBasis (fun s => s ∈ l) id; базис задается собственными элементами.

LaTeX

$$basis_sets (l : Filter α) : l.HasBasis (fun s : Set α => s ∈ l) id$$

Lean4

theorem ge_iff (hl' : l'.HasBasis p' s') : l ≤ l' ↔ ∀ i', p' i' → s' i' ∈ l :=
  ⟨fun h _i' hi' => h <| hl'.mem_of_mem hi', fun h _s hs =>
    let ⟨_i', hi', hs⟩ := hl'.mem_iff.1 hs
    mem_of_superset (h _ hi') hs⟩

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