eq_bot_iff — Mathlib

English

A HasBasis l with p s equals bottom iff some i has p i and s i is empty.

Русский

Базис HasBasis l с p s равен нулю тогда и только тогда, когда существует i с p i и s i пусто.

LaTeX

$$$l HasBasis p s \rightarrow (l = \bot) \Leftrightarrow \exists i, p i \wedge s i = \emptyset$$$

Lean4

theorem eq_bot_iff (hl : l.HasBasis p s) : l = ⊥ ↔ ∃ i, p i ∧ s i = ∅ :=
  not_iff_not.1 <|
    neBot_iff.symm.trans <| hl.neBot_iff.trans <| by simp only [not_exists, not_and, nonempty_iff_ne_empty]

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