inf_eq_bot_iff — Mathlib

English

For a nonempty Finset s, s.inf f equals ⊥ iff there exists b ∈ s with f(b) = ⊥.

Русский

Для непустого Finset s: s.inf f = ⊥ ⇔ существует b ∈ s, f(b) = ⊥.

LaTeX

$$$s.Nonempty \rightarrow (s.inf f = \bot \iff \exists b \in s, f(b) = \bot)$$$

Lean4

protected theorem inf_eq_bot_iff {α : Type*} [LinearOrder α] [BoundedOrder α] {s : Finset ι} {f : ι → α}
    (h : s.Nonempty) : s.inf f = ⊥ ↔ ∃ b ∈ s, f b = ⊥ :=
  h.sup_eq_top_iff (α := αᵒᵈ)

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