En ℝ, min(a,b) = min(b,a)
Demostrar con Lean4 que si \(a\) y \(b\) números reales, entonces \(\min(a, b) = \min(b, a)\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : min a b = min b a := by sorry |