sup_erase_bot — Mathlib

English

For a finite set s of α with a decidable equality, erasing the bottom element does not change the supremum of the identity function.

Русский

Пусть s — конечное множество элементов α; удаление нижнего элемента ⊥ из s не меняет суpремум для функции-id.

LaTeX

$$$ (s.\text{erase } \bot).sup id = s.sup id $$$

Lean4

@[simp]
theorem sup_erase_bot [DecidableEq α] (s : Finset α) : (s.erase ⊥).sup id = s.sup id :=
  by
  refine (sup_mono (s.erase_subset _)).antisymm (Finset.sup_le_iff.2 fun a ha => ?_)
  obtain rfl | ha' := eq_or_ne a ⊥
  · exact bot_le
  · exact le_sup (mem_erase.2 ⟨ha', ha⟩)

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