inf_eq_bot_iff — Mathlib

English

In a bounded and nontrivial linear order, s.inf f equals the bottom iff there exists b ∈ s with f(b) = ⊥.

Русский

В линейном порядке с нижним элементом и ненулевым, s.inf f = ⊥ тогда и только тогда, когда существует b ∈ s such that f(b) = ⊥.

LaTeX

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

Lean4

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

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