min_eq_iff — Mathlib

English

min(a,b) = c iff (a = c and a ≤ b) or (b = c and b ≤ a).

Русский

min(a,b) = c тогда и только тогда, когда (a = c и a ≤ b) или (b = c и b ≤ a).

LaTeX

$$$$\min(a,b) = c \iff (a = c \land a \le b) \lor (b = c \land b \le a).$$$$

Lean4

theorem min_eq_iff : min a b = c ↔ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a :=
  by
  constructor
  · intro h
    refine Or.imp (fun h' => ?_) (fun h' => ?_) (le_total a b) <;> exact ⟨by simpa [h'] using h, h'⟩
  · rintro (⟨rfl, h⟩ | ⟨rfl, h⟩) <;> simp [h]

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