hasBasis_self — Mathlib

English

A HasBasis l with predicate on s is equivalent to a covering property: for every t ∈ l there exists r ∈ l with r ⊆ t and P(r).

Русский

У базиса HasBasis l с условием на s эквивалентно, что для каждого t ∈ l существует r ∈ l с r ⊆ t и P(r).

LaTeX

$$HasBasis l (s ↦ (s ∈ l) ∧ P(s)) id ↔ ∀ t ∈ l, ∃ r ∈ l, P(r) ∧ r ⊆ t$$

Lean4

theorem hasBasis_self {l : Filter α} {P : Set α → Prop} :
    HasBasis l (fun s => s ∈ l ∧ P s) id ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t :=
  by
  simp only [hasBasis_iff, id, and_assoc]
  exact forall_congr' fun s => ⟨fun h => h.1, fun h => ⟨h, fun ⟨t, hl, _, hts⟩ => mem_of_superset hl hts⟩⟩

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