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 .
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura
-/
import Mathlib.Init.Algebra.Order
universe u
section
variable { α : Type u } [ LinearOrder : Type ?u.3811 → Type ?u.3811 α ]
lemma min_def ( a b : α ) : min : {α : Type ?u.17} → [self : Min α α → α → α a b = if a ≤ b then a else b := LinearOrder.min_def : ∀ {α : Type ?u.70} [self : LinearOrder α a b : α ), min a b = if a ≤ b a else b ..
lemma min_le_left ( a b : α ) : min : {α : Type ?u.104} → [self : Min α α → α → α a b ≤ a := by
if h : a ≤ b
then simp [ min_def , if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.210} {t e : α }, (if c then t else e ) = t h , le_refl ]
else simp [ min_def , if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.508} {t e : α }, (if c then t else e ) = e h ] ; exact le_of_not_le h
lemma min_le_right : ∀ (a b : α ), min a b ≤ b min_le_right ( a b : α ) : min : {α : Type ?u.708} → [self : Min α α → α → α a b ≤ b := by
if h : a ≤ b
then simp [ min_def , if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.814} {t e : α }, (if c then t else e ) = t h ] ; exact h
else simp [ min_def , if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.1042} {t e : α }, (if c then t else e ) = e h , le_refl ]
lemma le_min : ∀ {a b c : α }, c ≤ a c ≤ b c ≤ min a b le_min { a b c : α } ( h₁ : c ≤ a ) ( h₂ : c ≤ b ) : c ≤ min : {α : Type ?u.1309} → [self : Min α α → α → α a b := by
if h : a ≤ b
then simp [ min_def , if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.1402} {t e : α }, (if c then t else e ) = t h ] ; exact h₁
else simp [ min_def , if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.1628} {t e : α }, (if c then t else e ) = e h ] ; exact h₂
lemma max_def ( a b : α ) : max : {α : Type ?u.1812} → [self : Max α α → α → α a b = if a ≤ b then b else a := LinearOrder.max_def : ∀ {α : Type ?u.1865} [self : LinearOrder α a b : α ), max a b = if a ≤ b b else a ..
lemma le_max_left : ∀ (a b : α ), a ≤ max a b le_max_left ( a b : α ) : a ≤ max : {α : Type ?u.1899} → [self : Max α α → α → α a b := by
if h : a ≤ b
then simp [ max_def , if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.2005} {t e : α }, (if c then t else e ) = t h ] ; exact h
else simp [ max_def , if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.2231} {t e : α }, (if c then t else e ) = e h , le_refl ]
lemma le_max_right ( a b : α ) : b ≤ max : {α : Type ?u.2465} → [self : Max α α → α → α a b := by
if h : a ≤ b
then simp [ max_def , if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.2571} {t e : α }, (if c then t else e ) = t h , le_refl ]
else simp [ max_def , if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.2850} {t e : α }, (if c then t else e ) = e h ] ; exact le_of_not_le h
lemma max_le { a b c : α } ( h₁ : a ≤ c ) ( h₂ : b ≤ c ) : max : {α : Type ?u.3074} → [self : Max α α → α → α a b ≤ c := by
if h : a ≤ b
then simp [ max_def , if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.3167} {t e : α }, (if c then t else e ) = t h ] ; exact h₂
else simp [ max_def , if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.3395} {t e : α }, (if c then t else e ) = e h ] ; exact h₁
lemma eq_min : ∀ {a b c : α }, c ≤ a c ≤ b (∀ {d : α }, d ≤ a d ≤ b d ≤ c ) → c = min a b eq_min { a b c : α } ( h₁ : c ≤ a ) ( h₂ : c ≤ b ) ( h₃ : ∀ {d : α }, d ≤ a d ≤ b d ≤ c h₃ : ∀{ d }, d ≤ a → d ≤ b → d ≤ c ) :
c = min : {α : Type ?u.3634} → [self : Min α α → α → α a b :=
le_antisymm ( le_min h₁ h₂ ) ( h₃ : ∀ {d : α }, d ≤ a d ≤ b d ≤ c h₃ ( min_le_left a b ) ( min_le_right a b ))
lemma min_comm : ∀ (a b : α ), min a b = min b a min_comm ( a b : α ) : min : {α : Type ?u.3727} → [self : Min α α → α → α a b = min : {α : Type ?u.3739} → [self : Min α α → α → α b a :=
eq_min : ∀ {α : Type ?u.3746} [inst : LinearOrder α a b c : α },
c ≤ a c ≤ b (∀ {d : α }, d ≤ a d ≤ b d ≤ c ) → c = min a b ( min_le_right a b ) ( min_le_left a b ) (λ { _ } h₁ h₂ => le_min h₂ h₁ )
lemma min_assoc ( a b c : α ) : min : {α : Type ?u.3821} → [self : Min α α → α → α ( min : {α : Type ?u.3824} → [self : Min α α → α → α a b ) c = min : {α : Type ?u.3839} → [self : Min α α → α → α a ( min : {α : Type ?u.3842} → [self : Min α α → α → α b c ) :=
by apply eq_min : ∀ {α : Type ?u.3855} [inst : LinearOrder α a b c : α },
c ≤ a c ≤ b (∀ {d : α }, d ≤ a d ≤ b d ≤ c ) → c = min a b
. apply le_trans : ∀ {α : Type ?u.3883} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c ; apply min_le_left ; apply min_le_left
. apply le_min ; apply le_trans : ∀ {α : Type ?u.3975} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c h₂.h₁.a h₂.h₁.a h₂.h₁.b α
h₂.h₂ ; h₂.h₁.a h₂.h₁.a h₂.h₁.b α
h₂.h₂ apply min_le_left ; apply min_le_right ; apply min_le_right
. intros d h₁ h₂ ; apply le_min ; apply le_min h₁ ; apply le_trans : ∀ {α : Type ?u.4098} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c h₂ ; apply min_le_left ;
apply le_trans : ∀ {α : Type ?u.4130} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c h₂ ; apply min_le_right
lemma min_left_comm : @ LeftCommutative : {α : Type ?u.4177} → {β : Type ?u.4176} → (α → β → β Prop α α min : {α : Type ?u.4178} → [self : Min α α → α → α :=
left_comm min : {α : Type ?u.4202} → [self : Min α α → α → α (@ min_comm α _) (@ min_assoc α _)
@[ simp ]
lemma min_self ( a : α ) : min : {α : Type ?u.4245} → [self : Min α α → α → α a a = a := by simp [ min_def ]
lemma min_eq_left : ∀ {a b : α }, a ≤ b min a b = a min_eq_left { a b : α } ( h : a ≤ b ) : min : {α : Type ?u.4505} → [self : Min α α → α → α a b = a :=
by apply Eq.symm : ∀ {α : Sort ?u.4521} {a b : α }, a = b b = a ; apply eq_min : ∀ {α : Type ?u.4533} [inst : LinearOrder α a b c : α },
c ≤ a c ≤ b (∀ {d : α }, d ≤ a d ≤ b d ≤ c ) → c = min a b ( le_refl _ ) h h ∀ {d : α }, d ≤ a d ≤ b d ≤ a ; h ∀ {d : α }, d ≤ a d ≤ b d ≤ a intros ; assumption
lemma min_eq_right : ∀ {a b : α }, b ≤ a min a b = b min_eq_right { a b : α } ( h : b ≤ a ) : min : {α : Type ?u.4651} → [self : Min α α → α → α a b = b :=
by rw [ min_comm ]
exact min_eq_left h
lemma eq_max : ∀ {α : Type u} [inst : LinearOrder α a b c : α }, a ≤ c b ≤ c (∀ {d : α }, a ≤ d b ≤ d c ≤ d ) → c = max a b eq_max { a b c : α } ( h₁ : a ≤ c ) ( h₂ : b ≤ c ) ( h₃ : ∀ {d : α }, a ≤ d b ≤ d c ≤ d h₃ : ∀{ d }, a ≤ d → b ≤ d → c ≤ d ) :
c = max : {α : Type ?u.4773} → [self : Max α α → α → α a b :=
le_antisymm ( h₃ : ∀ {d : α }, a ≤ d b ≤ d c ≤ d h₃ ( le_max_left a b ) ( le_max_right a b )) ( max_le h₁ h₂ )
lemma max_comm : ∀ (a b : α ), max a b = max b a max_comm ( a b : α ) : max : {α : Type ?u.4866} → [self : Max α α → α → α a b = max : {α : Type ?u.4878} → [self : Max α α → α → α b a :=
eq_max : ∀ {α : Type ?u.4885} [inst : LinearOrder α a b c : α },
a ≤ c b ≤ c (∀ {d : α }, a ≤ d b ≤ d c ≤ d ) → c = max a b ( le_max_right a b ) ( le_max_left a b ) (λ { _ } h₁ h₂ => max_le h₂ h₁ )
lemma max_assoc ( a b c : α ) : max : {α : Type ?u.4960} → [self : Max α α → α → α ( max : {α : Type ?u.4963} → [self : Max α α → α → α a b ) c = max : {α : Type ?u.4978} → [self : Max α α → α → α a ( max : {α : Type ?u.4981} → [self : Max α α → α → α b c ) := by
apply eq_max : ∀ {α : Type ?u.4994} [inst : LinearOrder α a b c : α },
a ≤ c b ≤ c (∀ {d : α }, a ≤ d b ≤ d c ≤ d ) → c = max a b
· apply le_trans : ∀ {α : Type ?u.5022} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c ; apply le_max_left a b ; apply le_max_left
· apply max_le ; apply le_trans : ∀ {α : Type ?u.5102} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c h₂.h₁.a h₂.h₁.a h₂.h₁.b α
h₂.h₂ ; h₂.h₁.a h₂.h₁.a h₂.h₁.b α
h₂.h₂ apply le_max_right a b ; apply le_max_left ; apply le_max_right
· intros d h₁ h₂ ; apply max_le ; apply max_le h₁ ; apply le_trans : ∀ {α : Type ?u.5205} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c ( le_max_left _ _ ) h₂ ;
apply le_trans : ∀ {α : Type ?u.5249} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c ( le_max_right _ _ ) h₂
lemma max_left_comm : ∀ ( a b c : α ), max : {α : Type ?u.5315} → [self : Max α α → α → α a ( max : {α : Type ?u.5318} → [self : Max α α → α → α b c ) = max : {α : Type ?u.5333} → [self : Max α α → α → α b ( max : {α : Type ?u.5336} → [self : Max α α → α → α a c ) :=
left_comm max : {α : Type ?u.5346} → [self : Max α α → α → α (@ max_comm α _) (@ max_assoc α _)
@[ simp ] lemma max_self ( a : α ) : max : {α : Type ?u.5392} → [self : Max α α → α → α a a = a := by simp [ max_def ]
lemma max_eq_left : ∀ {a b : α }, b ≤ a max a b = a max_eq_left { a b : α } ( h : b ≤ a ) : max : {α : Type ?u.5652} → [self : Max α α → α → α a b = a :=
by apply Eq.symm : ∀ {α : Sort ?u.5668} {a b : α }, a = b b = a ; apply eq_max : ∀ {α : Type ?u.5680} [inst : LinearOrder α a b c : α },
a ≤ c b ≤ c (∀ {d : α }, a ≤ d b ≤ d c ≤ d ) → c = max a b ( le_refl _ ) h h ∀ {d : α }, a ≤ d b ≤ d a ≤ d ; h ∀ {d : α }, a ≤ d b ≤ d a ≤ d intros ; assumption
lemma max_eq_right { a b : α } ( h : a ≤ b ) : max : {α : Type ?u.5798} → [self : Max α α → α → α a b = b :=
by rw [ ← max_comm b a ] ; exact max_eq_left h
/- these rely on lt_of_lt -/
lemma min_eq_left_of_lt : ∀ {a b : α }, a < b min a b = a min_eq_left_of_lt { a b : α } ( h : a < b ) : min : {α : Type ?u.5880} → [self : Min α α → α → α a b = a :=
min_eq_left ( le_of_lt : ∀ {α : Type ?u.5909} [inst : Preorder α a b : α }, a < b a ≤ b h )
lemma min_eq_right_of_lt : ∀ {a b : α }, b < a min a b = b min_eq_right_of_lt { a b : α } ( h : b < a ) : min : {α : Type ?u.5976} → [self : Min α α → α → α a b = b :=
min_eq_right ( le_of_lt : ∀ {α : Type ?u.6005} [inst : Preorder α a b : α }, a < b a ≤ b h )
lemma max_eq_left_of_lt : ∀ {a b : α }, b < a max a b = a max_eq_left_of_lt { a b : α } ( h : b < a ) : max : {α : Type ?u.6072} → [self : Max α α → α → α a b = a :=
max_eq_left ( le_of_lt : ∀ {α : Type ?u.6101} [inst : Preorder α a b : α }, a < b a ≤ b h )
lemma max_eq_right_of_lt : ∀ {a b : α }, a < b max a b = b max_eq_right_of_lt { a b : α } ( h : a < b ) : max : {α : Type ?u.6168} → [self : Max α α → α → α a b = b :=
max_eq_right ( le_of_lt : ∀ {α : Type ?u.6197} [inst : Preorder α a b : α }, a < b a ≤ b h )
/- these use the fact that it is a linear ordering -/
lemma lt_min : ∀ {a b c : α }, a < b a < c a < min b c lt_min { a b c : α } ( h₁ : a < b ) ( h₂ : a < c ) : a < min : {α : Type ?u.6271} → [self : Min α α → α → α b c :=
Or.elim : ∀ {a b c : Prop }, a ∨ b (a → c (b → c c ( le_or_gt b c )
(λ h : b ≤ c => by rwa [ min_eq_left h ] )
(λ h : b > c => by rwa [ min_eq_right_of_lt h ] )
lemma max_lt { a b c : α } ( h₁ : a < c ) ( h₂ : b < c ) : max : {α : Type ?u.6423} → [self : Max α α → α → α a b < c :=
Or.elim : ∀ {a b c : Prop }, a ∨ b (a → c (b → c c ( le_or_gt a b )
(λ h : a ≤ b => by rwa [ max_eq_right h ] )
(λ h : a > b => by rwa [ max_eq_left_of_lt h ] )
end