bot_mem — Mathlib

English

In a max chain, the bottom element belongs to the chain when an bottom exists.

Русский

В максимальной цепи нижний элемент принадлежит цепи, если он существует.

LaTeX

$$$ IsMaxChain\\ (\\le)\\ s \\rightarrow ⊥ \\in s $$$

Lean4

theorem bot_mem [LE α] [OrderBot α] (h : IsMaxChain (· ≤ ·) s) : ⊥ ∈ s :=
  (h.2 (h.1.insert fun _ _ _ => Or.inl bot_le) <| subset_insert _ _).symm ▸ mem_insert _ _

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