eq_max — Mathlib

English

Let α be a linear order. If a ≤ c and b ≤ c and for all d with a ≤ d and b ≤ d, we have c ≤ d, then c = max(a,b).

Русский

Пусть α — линейно упорядоченное множество. Если a ≤ c, b ≤ c, и для всякого d, если a ≤ d и b ≤ d, то c ≤ d, тогда c = max(a,b).

LaTeX

$$$ (a \le c) \land (b \le c) \land (\forall d, (a \le d \land b \le d) \rightarrow c \le d) \Rightarrow c = \max(a,b) $$$

Lean4

theorem eq_max (h₁ : a ≤ c) (h₂ : b ≤ c) (h₃ : ∀ {d}, a ≤ d → b ≤ d → c ≤ d) : c = max a b :=
  le_antisymm (h₃ (le_max_left a b) (le_max_right a b)) (max_le h₁ h₂)

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