max'_eq_iff — Mathlib

English

For nonempty S and a ∈ S, s.max' H = a iff a ∈ S and every b ∈ S satisfies b ≤ a.

Русский

Для непустого S и a ∈ S: s.max' H = a тогда и только тогда, когда a ∈ S и каждый b ∈ S удовлетворяет b ≤ a.

LaTeX

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

Lean4

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

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