min'_eq_iff — Mathlib

English

For nonempty S and a ∈ S, s.min' H = a iff a ∈ S and a is ≤ every element of S.

Русский

Для непустого S и a ∈ S: s.min' H = a тогда и только тогда, когда a ∈ S и a ≤ каждое элемент S.

LaTeX

$$$$s.min' H = a \iff a \in s \land \forall b \in s, a \le b.$$$$

Lean4

theorem min'_eq_iff (a : α) : s.min' H = a ↔ a ∈ s ∧ ∀ (b : α), b ∈ s → a ≤ b :=
  ⟨(· ▸ ⟨min'_mem _ _, min'_le _⟩), fun h ↦ le_antisymm (min'_le _ _ h.1) (le_min' _ _ _ h.2)⟩

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