LeanPool.LeanPolyABC.Lib.Max3

Imported Lean Pool material for LeanPool.LeanPolyABC.Lib.Max3.

def Nat.max₃ (a b c : Nat) : Nat

The maximum of three natural numbers, max (max a b) c.

Equations

• a.max₃ b c = max (max a b) c

theorem Nat.max₃_mul_distrib_left (a b c d : Nat) : a * b.max₃ c d = (a * b).max₃ (a * c) (a * d)

theorem Nat.max₃_add_distrib_left (a b c d : Nat) : d + a.max₃ b c = (d + a).max₃ (d + b) (d + c)

theorem Nat.max₃_add_distrib_right (a b c d : Nat) : a.max₃ b c + d = (a + d).max₃ (b + d) (c + d)

theorem Nat.le_max₃_left (a b c : Nat) : a ≤ a.max₃ b c

theorem Nat.le_max₃_middle (a b c : Nat) : b ≤ a.max₃ b c

theorem Nat.le_max₃_right (a b c : Nat) : c ≤ a.max₃ b c

theorem Nat.max₃_lt {a b c d : Nat} : a.max₃ b c < d ↔ a < d ∧ b < d ∧ c < d

theorem Nat.max₃_le {a b c d : Nat} : a.max₃ b c ≤ d ↔ a ≤ d ∧ b ≤ d ∧ c ≤ d