inf_eq_top_iff — Mathlib

English

For a finite set s and f: β → α, s.inf f = ⊤ if and only if f(b) = ⊤ for all b ∈ s.

Русский

Для конечного множества s и функции f: β → α, инфимум по s равен ⊤ тогда и только тогда, когда f(b) = ⊤ для всех b ∈ s.

LaTeX

$$$ s.\\inf f = ⊤ \\iff \\forall b \\in s, f(b) = ⊤ $$$

Lean4

@[simp]
protected theorem inf_eq_top_iff (f : β → α) (S : Finset β) : S.inf f = ⊤ ↔ ∀ s ∈ S, f s = ⊤ :=
  @Finset.sup_eq_bot_iff αᵒᵈ _ _ _ _ _

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