hasBasis_biInf_principal' — Mathlib

English

Given a family s with a predicate p, and the directed relation among indices, the biInf of principal(s i) has a basis under p with s.

Русский

При наличии предиката p на индексах и направленной зависимости биInf от principal(s i) имеет базис при p с использованием s.

LaTeX

$$$ (\iInf i, p(i) \land 𝓟(s(i))).HasBasis p s $$$

Lean4

theorem hasBasis_biInf_principal' {ι : Type*} {p : ι → Prop} {s : ι → Set α}
    (h : ∀ i, p i → ∀ j, p j → ∃ k, p k ∧ s k ⊆ s i ∧ s k ⊆ s j) (ne : ∃ i, p i) :
    (⨅ (i) (_ : p i), 𝓟 (s i)).HasBasis p s :=
  Filter.hasBasis_biInf_principal h ne

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