neBot_iff — Mathlib

English

A filter with HasBasis p s is nontrivial (not bottom) iff every relevant basis set s i is nonempty.

Русский

Фильтр с базисом HasBasis p s непустой (не ноль), если и только каждый соответствующий элемент базиса s i непуст.

LaTeX

$$$\text{HasBasis } l (p,s) \Rightarrow (l\text{ NeBot}) \Leftrightarrow \forall i, p i \to (s i)\neq \emptyset$$$

Lean4

protected theorem neBot_iff (hl : l.HasBasis p s) : NeBot l ↔ ∀ {i}, p i → (s i).Nonempty :=
  forall_mem_nonempty_iff_neBot.symm.trans <| hl.forall_iff fun _ _ => Nonempty.mono

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