eq_min — Mathlib

English

If c ≤ a and c ≤ b and ∀ d, d ≤ a ∧ d ≤ b → d ≤ c, then c = min a b.

Русский

Если c ≤ a и c ≤ b и для всех d, если d ≤ a и d ≤ b, то d ≤ c, то c = min(a,b).

LaTeX

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

Lean4

theorem eq_min (h₁ : c ≤ a) (h₂ : c ≤ b) (h₃ : ∀ {d}, d ≤ a → d ≤ b → d ≤ c) : c = min a b :=
  le_antisymm (le_min h₁ h₂) (h₃ (min_le_left a b) (min_le_right a b))

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