sup_eq_bot_of_isEmpty — Mathlib

English

If the index type β is empty, then the supremum of any function f over a finite set S is the bottom element.

Русский

Если индексный тип β пуст, то супремум по S от любой функции f равен ⊥.

LaTeX

$$$[IsEmpty\,\beta] (f : \beta \to \alpha) (S : Finset \beta) : S.sup f = \bot$$$

Lean4

@[simp]
theorem sup_eq_bot_of_isEmpty [IsEmpty β] (f : β → α) (S : Finset β) : S.sup f = ⊥ :=
  by
  rw [Finset.sup_eq_bot_iff]
  exact fun x _ => False.elim <| IsEmpty.false x

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