inf_basis_neBot_iff — Mathlib

English

For a basis of l, NeBot(l ⊓ l') is equivalent to the property that every basis element of l and every basis element of l' intersect nontrivially.

Русский

Для базиса l небот равенство с l' эквивалентно тому, что каждое базисное множество l пересекается с любым базисным множеством l'.

LaTeX

$$$\\text{Inf NeBot Iff}\\left(l, l'\\right) \\iff \\forall i, p i \\to \\forall i', p' i' \\to (s i \\cap s' i').Nonempty$$$

Lean4

theorem inf_basis_neBot_iff (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
    NeBot (l ⊓ l') ↔ ∀ ⦃i⦄, p i → ∀ ⦃i'⦄, p' i' → (s i ∩ s' i').Nonempty :=
  (hl.inf' hl').neBot_iff.trans <| by simp [@forall_swap _ ι']

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