ne_bot_iff — Mathlib

English

A filter f is not bottom if and only if every realization F a is nonempty.

Русский

Фильтр f не равен нижней границе тогда и только тогда, когда каждый элемент реализации F a не пуст.

LaTeX

$$$f \\neq \\bot \\iff \\forall a : F.σ, (F.F a).Nonempty$$$

Lean4

theorem ne_bot_iff {f : Filter α} (F : f.Realizer) : f ≠ ⊥ ↔ ∀ a : F.σ, (F.F a).Nonempty :=
  by
  rw [not_iff_comm, ← le_bot_iff, F.le_iff Realizer.bot, not_forall]
  simp only [Set.not_nonempty_iff_eq_empty]
  exact
    ⟨fun ⟨x, e⟩ _ ↦ ⟨x, le_of_eq e⟩, fun h ↦
      let ⟨x, h⟩ := h ()
      ⟨x, le_bot_iff.1 h⟩⟩

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