le_min_iff — Mathlib

English

Let s be a nonempty subset of a linear order α such that s is well-founded. Then for any element a ∈ α, a is below the minimum of s if and only if a is below every element of s.

Русский

Пусть s ⊆ α, где α — линейный порядок, и s не пусто и хорошо основанно. Тогда для любого a ∈ α верно: a меньше или равно минимальному элементу s тогда и только если a ≤ каждый элемент s.

LaTeX

$$$a \le hs.min hsn \iff \forall b, b \in s \rightarrow a \le b$$$

Lean4

theorem le_min_iff (hs : s.IsWF) (hn : s.Nonempty) : a ≤ hs.min hn ↔ ∀ b, b ∈ s → a ≤ b :=
  ⟨fun ha _b hb => le_trans ha (hs.min_le hn hb), fun h => h _ (hs.min_mem _)⟩

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