@[instance_reducible]

instance Fin.instMin {n : Nat} : Min (Fin n)

Equations

• Fin.instMin = { min := fun (a b : Fin n) => ⟨min ↑a ↑b, ⋯⟩ }

@[instance_reducible]

instance Fin.instMax {n : Nat} : Max (Fin n)

Equations

• Fin.instMax = { max := fun (a b : Fin n) => ⟨max ↑a ↑b, ⋯⟩ }

@[simp]

theorem Fin.val_min {n : Nat} (a b : Fin n) : ↑(min a b) = min ↑a ↑b

@[simp]

theorem Fin.val_max {n : Nat} (a b : Fin n) : ↑(max a b) = max ↑a ↑b