Documentation
LeanCourse
.
MIL
.
C02_Basics
.
S04_More_on_Order_and_Divisibility
Search
Google site search
return to top
source
Imports
Init
LeanCourse.Common
Mathlib.Data.Real.Basic
Imported by
C02S04
.
aux
source
theorem
C02S04
.
aux
(a :
ℝ
)
(b :
ℝ
)
(c :
ℝ
)
:
min
a
b
+
c
≤
min
(
a
+
c
)
(
b
+
c
)