sup_eq_bot_iff — Mathlib

English

For any f, the supremum over a finite set S equals the bottom element if and only if every element of S maps to bottom under f.

Русский

Супремум по конечному множеству S равен ⊥ тогда и только тогда, когда для каждого s ∈ S выполняется f(s) = ⊥.

LaTeX

$$$S.sup f = \bot \;\Leftrightarrow\; \forall s \in S, f s = \bot$$$

Lean4

@[simp]
protected theorem sup_eq_bot_iff (f : β → α) (S : Finset β) : S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥ := by
  classical induction S using Finset.induction <;> simp [*]

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