inf_neBot_iff — Mathlib

English

The NeBot status of l ⨅ principal s is equivalent to the universal nonemptiness of intersections s_i ∩ s over the base elements.

Русский

Статус NeBot для l ⨅ principal s эквивалентен тому, что пересечения s_i ∩ s непусты для всех базисных элементов.

LaTeX

$$$\\text{NeBot}(l \\inf \\mathcal{P}s) \\iff \\forall i, p i \\to (s i \\cap s).Nonempty$$$

Lean4

theorem inf_neBot_iff : NeBot (l ⊓ l') ↔ ∀ ⦃s : Set α⦄, s ∈ l → ∀ ⦃s'⦄, s' ∈ l' → (s ∩ s').Nonempty :=
  l.basis_sets.inf_neBot_iff

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