Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
namespace Mt.Utils.Nat
theorem max_of_le { a b : Nat } : a ≤ b → a . max b = b := by
intro h ; simp only [ Nat.max , h , ite_true : ∀ {α : Sort ?u.39 } (a b : α ), (if True then a else b ) = a ]
theorem max_of_eq' { a b : Nat } : a = b → a . max b = b :=
λ h => max_of_le ( by rw [ h ] ; constructor )
theorem max_of_eq { a b : Nat } : a = b → a . max b = a := by
intro h ; rw [ max_of_eq' h ] ; exact h . symm : ∀ {α : Sort ?u.194 } {a b : α }, a = b b = a
theorem max_of_gt { a b : Nat } : a > b → a . max b = a := by
intro h ; simp only [ Nat.max , Nat.not_le_of_gt : ∀ {n m : Nat }, n > m ¬ n ≤ m h , ite_false : ∀ {α : Sort ?u.252 } (a b : α ), (if False then a else b ) = b ]
theorem max_of_ge { a b : Nat } : a ≥ b → a . max b = a := by
intro h
cases Nat.eq_or_lt_of_le : ∀ {n m : Nat }, n ≤ m n = m ∨ n < m h <;> rename_i h
. exact max_of_eq h . symm : ∀ {α : Sort ?u.440 } {a b : α }, a = b b = a
. exact max_of_gt h
theorem max_of_lt { a b : Nat } : a < b → a . max b = b := max_of_le ∘ Nat.le_of_lt : ∀ {n m : Nat }, n < m n ≤ m
theorem max_comm : ∀ a b : Nat , a . max b = b . max a := by
intro a b
cases Nat.lt_or_ge : ∀ (n m : Nat ), n < m ∨ n ≥ m a b <;> rename_i h
. rw [ max_of_lt h , max_of_gt h ]
cases Nat.eq_or_lt_of_le : ∀ {n m : Nat }, n ≤ m n = m ∨ n < m h <;> ( clear h ; rename_i h )
. rw [ max_of_eq h , max_of_eq' h . symm : ∀ {α : Sort ?u.695 } {a b : α }, a = b b = a ]
. rw [ max_of_lt h , max_of_gt h ]
theorem max_assoc : ∀ a b c : Nat , ( a . max b ). max c = a . max ( b . max c ) := by
intros a b c
cases Nat.lt_or_ge : ∀ (n m : Nat ), n < m ∨ n ≥ m a b
<;> cases Nat.lt_or_ge : ∀ (n m : Nat ), n < m ∨ n ≥ m b c
<;> rename_i ab bc a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr
. a, b, c : Nat ab : a < b bc : b < c inl.inl a, b, c : Nat ab : a < b bc : b < c inl.inl a, b, c : Nat ab : a < b bc : b ≥ c inl.inr a, b, c : Nat ab : a ≥ b bc : b < c inr.inl a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr rw [ a, b, c : Nat ab : a < b bc : b < c inl.inl max_of_lt ab , a, b, c : Nat ab : a < b bc : b < c inl.inl a, b, c : Nat ab : a < b bc : b < c inl.inl max_of_lt bc , a, b, c : Nat ab : a < b bc : b < c inl.inl a, b, c : Nat ab : a < b bc : b < c inl.inl max_of_lt ( trans : ∀ {α : Sort ?u.973 } {β : Sort ?u.972 } {γ : Sort ?u.971 } {r : α → β → Sort ?u.976 s : β → γ → Sort ?u.975 t : α → γ → Sort ?u.974 self : Trans r s t a : α } {b : β } {c : γ }, r a b s b c t a c ab bc ) a, b, c : Nat ab : a < b bc : b < c inl.inl ]
. a, b, c : Nat ab : a < b bc : b ≥ c inl.inr a, b, c : Nat ab : a < b bc : b ≥ c inl.inr a, b, c : Nat ab : a ≥ b bc : b < c inr.inl a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr rw [ a, b, c : Nat ab : a < b bc : b ≥ c inl.inr max_of_lt ab , a, b, c : Nat ab : a < b bc : b ≥ c inl.inr a, b, c : Nat ab : a < b bc : b ≥ c inl.inr max_of_ge bc , a, b, c : Nat ab : a < b bc : b ≥ c inl.inr a, b, c : Nat ab : a < b bc : b ≥ c inl.inr max_of_lt ab a, b, c : Nat ab : a < b bc : b ≥ c inl.inr ]
. a, b, c : Nat ab : a ≥ b bc : b < c inr.inl a, b, c : Nat ab : a ≥ b bc : b < c inr.inl a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr rw [ a, b, c : Nat ab : a ≥ b bc : b < c inr.inl max_of_ge ab , a, b, c : Nat ab : a ≥ b bc : b < c inr.inl a, b, c : Nat ab : a ≥ b bc : b < c inr.inl max_of_lt bc a, b, c : Nat ab : a ≥ b bc : b < c inr.inl ]
. a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr rw [ a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr max_of_ge ab , a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr max_of_ge bc , a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr max_of_ge ab a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr ] a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr
a, b, c : Nat ab : a ≥ b bc : b ≥ c inr.inr exact max_of_ge ( trans : ∀ {α : Sort ?u.1082 } {β : Sort ?u.1081 } {γ : Sort ?u.1080 } {r : α → β → Sort ?u.1085 s : β → γ → Sort ?u.1084 t : α → γ → Sort ?u.1083 self : Trans r s t a : α } {b : β } {c : γ }, r a b s b c t a c bc ab : c ≤ a )
theorem zero_max : ∀ a : Nat , (( 0 : Nat ). max a ) = a := by
intro a
simp only [ Nat.max , Nat.zero_le : ∀ (n : Nat ), 0 ≤ n , ite_true : ∀ {α : Sort ?u.1179 } (a b : α ), (if True then a else b ) = a ]
theorem max_zero : ∀ a : Nat , ( a . max 0 ) = a := fun a => calc
( a . max 0 ) = Nat.max 0 a := max_comm ..
_ = a := zero_max a
theorem max_le { a b c : Nat } : a . max b ≤ c ↔ a ≤ c ∧ b ≤ c := by
constructor <;> intro h
<;> ( cases Nat.lt_or_ge : ∀ (n m : Nat ), n < m ∨ n ≥ m a b ) <;> rename_i ab
. mp.inl mp.inr a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a < b mpr.inl a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a ≥ b mpr.inr rw [ max_of_lt ab a, b, c : Nat h : b ≤ c ab : a < b mp.inl ] a, b, c : Nat h : b ≤ c ab : a < b mp.inl at h a, b, c : Nat h : b ≤ c ab : a < b mp.inl
mp.inl mp.inr a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a < b mpr.inl a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a ≥ b mpr.inr exact ⟨ Nat.le_of_lt : ∀ {n m : Nat }, n < m n ≤ m ( trans : ∀ {α : Sort ?u.1586 } {β : Sort ?u.1585 } {γ : Sort ?u.1584 } {r : α → β → Sort ?u.1589 s : β → γ → Sort ?u.1588 t : α → γ → Sort ?u.1587 self : Trans r s t a : α } {b : β } {c : γ }, r a b s b c t a c ab h ), h ⟩
. mp.inr a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a < b mpr.inl a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a ≥ b mpr.inr rw [ max_of_ge ab a, b, c : Nat h : a ≤ c ab : a ≥ b mp.inr ] a, b, c : Nat h : a ≤ c ab : a ≥ b mp.inr at h a, b, c : Nat h : a ≤ c ab : a ≥ b mp.inr
mp.inr a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a < b mpr.inl a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a ≥ b mpr.inr exact ⟨ h , trans : ∀ {α : Sort ?u.1667 } {β : Sort ?u.1666 } {γ : Sort ?u.1665 } {r : α → β → Sort ?u.1670 s : β → γ → Sort ?u.1669 t : α → γ → Sort ?u.1668 self : Trans r s t a : α } {b : β } {c : γ }, r a b s b c t a c ab h ⟩
. a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a < b mpr.inl a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a < b mpr.inl a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a ≥ b mpr.inr rw [ a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a < b mpr.inl max_of_lt ab a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a < b mpr.inl ] a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a < b mpr.inl
a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a < b mpr.inl a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a ≥ b mpr.inr exact h . right : ∀ {a b : Prop }, a ∧ b b
. a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a ≥ b mpr.inr a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a ≥ b mpr.inr rw [ a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a ≥ b mpr.inr max_of_ge ab a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a ≥ b mpr.inr ] a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a ≥ b mpr.inr
a, b, c : Nat h : a ≤ c ∧ b ≤ c ab : a ≥ b mpr.inr exact h . left : ∀ {a b : Prop }, a ∧ b a
end Mt.Utils.Nat