theorem Char.min_max_def {a b : Char} : (min a b = if a ≤ b then a else b) ∧ max a b = if a ≤ b then b else a

theorem Char.min_def {a b : Char} : min a b = if a ≤ b then a else b

theorem Char.max_def {a b : Char} : max a b = if a ≤ b then b else a

@[instance_reducible]

instance Char.instLinearOrder_projects : LinearOrder Char

Equations

• Char.instLinearOrder_projects = { toLE := Char.instLE, toLT := Char.instLT, le_refl := Char.le_refl, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯, toMin := minOfOrd', toMax := maxOfOrd', toOrd := instOrdChar, le_total := Char.le_total, toDecidableLE := fun (a b : Char) => inferInstance, toDecidableEq := decidableEqOfDecidableLE, toDecidableLT := decidableLTOfDecidableLE, min_def := ⋯, max_def := ⋯, compare_eq_compareOfLessAndEq := Char.instLinearOrder_projects._proof_1 }