generate_neBot_iff — Mathlib

English

The filter generate s is nontrivial (NeBot) iff for every t ⊆ s with t finite, t.sInter Nonempty.

Русский

Фильтр generate s не пустой эквивалентен тому, что для каждого конечного подмножества t ⊆ s их пересечение не пусто.

LaTeX

$$NeBot (generate s) ↔ ∀ t, t ⊆ s → t.Finite → (⋂₀ t).Nonempty.$$

Lean4

theorem generate_neBot_iff {s : Set (Set α)} : NeBot (generate s) ↔ ∀ t, t ⊆ s → t.Finite → (⋂₀ t).Nonempty :=
  (hasBasis_generate s).neBot_iff.trans <| by simp only [← and_imp, and_comm]

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