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) 2018 Johannes HΓΆlzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes HΓΆlzl, Floris van Doorn, Gabriel Ebner, Yury Kudryashov
! This file was ported from Lean 3 source module data.nat.lattice
! leanprover-community/mathlib commit 52fa514ec337dd970d71d8de8d0fd68b455a1e54
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.Interval
import Mathlib.Order.ConditionallyCompleteLattice.Finset
/-!
# Conditionally complete linear order structure on `β`
In this file we
* define a `ConditionallyCcompleteLinearOrderBot` structure on `β`;
* prove a few lemmas about `iSup`/`iInf`/`Set.iUnion`/`Set.iInter` and natural numbers.
-/
open Set
namespace Nat
open Classical
noncomputable instance : InfSet β :=
β¨ fun s β¦ if h : β n , n β s then @ Nat.find ( fun n β¦ n β s ) _ h else 0 β©
noncomputable instance : SupSet β :=
β¨ fun s β¦ if h : β n , β a β s , a β€ n then @ Nat.find ( fun n β¦ β a β s , a β€ n ) _ h else 0 β©
theorem sInf_def { s : Set β } ( h : s . Nonempty ) : sInf : {Ξ± : Type ?u.1488} β [self : InfSet Ξ± Set Ξ± Ξ± s = @ Nat.find ( fun n β¦ n β s ) _ h :=
dif_pos : β {c : Prop } {h : Decidable c hc : c ) {Ξ± : Sort ?u.1541} {t : c β Ξ± e : Β¬ c Ξ± dite c t e = t hc _
#align nat.Inf_def Nat.sInf_def
theorem sSup_def { s : Set β } ( h : β n , β a β s , a β€ n ) :
sSup : {Ξ± : Type ?u.1638} β [self : SupSet Ξ± Set Ξ± Ξ± s = @ Nat.find ( fun n β¦ β a β s , a β€ n ) _ h :=
dif_pos : β {c : Prop } {h : Decidable c hc : c ) {Ξ± : Sort ?u.2272} {t : c β Ξ± e : Β¬ c Ξ± dite c t e = t hc _
#align nat.Sup_def Nat.sSup_def
theorem _root_.Set.Infinite.Nat.sSup_eq_zero { s : Set β } ( h : s . Infinite ) : sSup : {Ξ± : Type ?u.2327} β [self : SupSet Ξ± Set Ξ± Ξ± s = 0 :=
dif_neg fun β¨ n , hn β© β¦
let β¨ k , hks , hk β© := h . exists_gt n
( hn k hks ). not_lt hk
#align set.infinite.nat.Sup_eq_zero Set.Infinite.Nat.sSup_eq_zero
@[ simp ]
theorem sInf_eq_zero { s : Set β } : sInf : {Ξ± : Type ?u.2916} β [self : InfSet Ξ± Set Ξ± Ξ± s = 0 β 0 β s β¨ s = β
:= by
cases eq_empty_or_nonempty s with
| inl : β {a b : Prop }, a β a β¨ b h => subst h
simp only [ or_true_iff , eq_self_iff_true : β {Ξ± : Sort ?u.3151} (a : Ξ± ), a = a β True , iff_true_iff , iInf : {Ξ± : Type ?u.3177} β [inst : InfSet Ξ± {ΞΉ : Sort ?u.3176} β (ΞΉ β Ξ± Ξ± , InfSet.sInf : {Ξ± : Type ?u.3184} β [self : InfSet Ξ± Set Ξ± Ξ± ,
mem_empty_iff_false , exists_false , dif_neg , not_false_iff ]
| inr : β {a b : Prop }, b β a β¨ b h => simp only [ h . ne_empty , or_false_iff , Nat.sInf_def , h , Nat.find_eq_zero ]
#align nat.Inf_eq_zero Nat.sInf_eq_zero
@[ simp ]
theorem sInf_empty : sInf : {Ξ± : Type ?u.4327} β [self : InfSet Ξ± Set Ξ± Ξ± β
= 0 := by
rw [ sInf_eq_zero ]
right
rfl
#align nat.Inf_empty Nat.sInf_empty
@[ simp ]
theorem iInf_of_empty { ΞΉ : Sort _ } [ IsEmpty ΞΉ ] ( f : ΞΉ β β ) : iInf : {Ξ± : Type ?u.4560} β [inst : InfSet Ξ± {ΞΉ : Sort ?u.4559} β (ΞΉ β Ξ± Ξ± f = 0 := by
rw [ iInf_of_empty' , sInf_empty ]
#align nat.infi_of_empty Nat.iInf_of_empty
theorem sInf_mem { s : Set β } ( h : s . Nonempty ) : sInf : {Ξ± : Type ?u.4773} β [self : InfSet Ξ± Set Ξ± Ξ± s β s := by
rw [ Nat.sInf_def h ]
exact Nat.find_spec h
#align nat.Inf_mem Nat.sInf_mem
theorem not_mem_of_lt_sInf { s : Set β } { m : β } ( hm : m < sInf : {Ξ± : Type ?u.4858} β [self : InfSet Ξ± Set Ξ± Ξ± s ) : m β s := by
cases eq_empty_or_nonempty s with
| inl : β {a b : Prop }, a β a β¨ b h => subst h ; apply not_mem_empty : β {Ξ± : Type ?u.4969} (x : Ξ± ), Β¬ x β β
| inr : β {a b : Prop }, b β a β¨ b h => rw [ Nat.sInf_def h ] at hm ; exact Nat.find_min h hm
#align nat.not_mem_of_lt_Inf Nat.not_mem_of_lt_sInf
protected theorem sInf_le { s : Set β } { m : β } ( hm : m β s ) : sInf : {Ξ± : Type ?u.5109} β [self : InfSet Ξ± Set Ξ± Ξ± s β€ m := by
rw [ Nat.sInf_def β¨ m , hm β© ]
exact Nat.find_min' β¨ m , hm β© hm
#align nat.Inf_le Nat.sInf_le
theorem nonempty_of_pos_sInf { s : Set β } ( h : 0 < sInf : {Ξ± : Type ?u.5292} β [self : InfSet Ξ± Set Ξ± Ξ± s ) : s . Nonempty := by
by_contra contra
rw [ Set.not_nonempty_iff_eq_empty ] at contra
have h' : sInf : {Ξ± : Type ?u.5580} β [self : InfSet Ξ± Set Ξ± Ξ± s β 0 := ne_of_gt : β {a b : β }, b < a a β b h
apply h'
rw [ Nat.sInf_eq_zero ]
right
assumption
#align nat.nonempty_of_pos_Inf Nat.nonempty_of_pos_sInf
theorem nonempty_of_sInf_eq_succ { s : Set β } { k : β } ( h : sInf : {Ξ± : Type ?u.5653} β [self : InfSet Ξ± Set Ξ± Ξ± s = k + 1 ) : s . Nonempty :=
nonempty_of_pos_sInf ( h . symm : β {Ξ± : Sort ?u.5779} {a b : Ξ± }, a = b b = a βΈ succ_pos k : sInf : {Ξ± : Type ?u.5749} β [self : InfSet Ξ± Set Ξ± Ξ± s > 0 )
#align nat.nonempty_of_Inf_eq_succ Nat.nonempty_of_sInf_eq_succ
theorem eq_Ici_of_nonempty_of_upward_closed { s : Set β } ( hs : s . Nonempty )
( hs' : β (kβ kβ : β ), kβ β€ kβ kβ β s kβ β s hs' : β kβ kβ : β , kβ β€ kβ β kβ β s β kβ β s ) : s = Ici ( sInf : {Ξ± : Type ?u.5891} β [self : InfSet Ξ± Set Ξ± Ξ± s ) :=
ext : β {Ξ± : Type ?u.6023} {a b : Set Ξ± (β (x : Ξ± ), x β a β x β b ) β a = b fun n β¦ β¨ fun H β¦ Nat.sInf_le H , fun H β¦ hs' : β (kβ kβ : β ), kβ β€ kβ kβ β s kβ β s hs' ( sInf : {Ξ± : Type ?u.6058} β [self : InfSet Ξ± Set Ξ± Ξ± s ) n H ( sInf_mem hs )β©
#align nat.eq_Ici_of_nonempty_of_upward_closed Nat.eq_Ici_of_nonempty_of_upward_closed
theorem sInf_upward_closed_eq_succ_iff { s : Set β } ( hs : β (kβ kβ : β ), kβ β€ kβ kβ β s kβ β s hs : β kβ kβ : β , kβ β€ kβ β kβ β s β kβ β s )
( k : β ) : sInf : {Ξ± : Type ?u.6181} β [self : InfSet Ξ± Set Ξ± Ξ± s = k + 1 β k + 1 β s β§ k β s := by
constructor
Β· intro H
rw [ eq_Ici_of_nonempty_of_upward_closed ( nonempty_of_sInf_eq_succ _ ) hs : β (kβ kβ : β ), kβ β€ kβ kβ β s kβ β s hs , H , mem_Ici , mem_Ici ]
exact β¨ le_rfl , k . not_succ_le_self β© ;
exact k ; assumption
Β· rintro β¨ H , H' β©
rw [ sInf_def (β¨ _ , H β© : s . Nonempty ), find_eq_iff ]
exact β¨ H , fun n hnk hns β¦ H' <| hs : β (kβ kβ : β ), kβ β€ kβ kβ β s kβ β s hs n k ( lt_succ_iff . mp : β {a b : Prop }, (a β b a β b hnk ) hns β©
#align nat.Inf_upward_closed_eq_succ_iff Nat.sInf_upward_closed_eq_succ_iff
/-- This instance is necessary, otherwise the lattice operations would be derived via
`ConditionallyCompleteLinearOrderBot` and marked as noncomputable. -/
instance : Lattice β :=
LinearOrder.toLattice
noncomputable instance : ConditionallyCompleteLinearOrderBot : Type ?u.7337 β Type ?u.7337 β :=
{ ( inferInstance : {Ξ± : Sort ?u.7347} β [i : Ξ± ] β Ξ± : OrderBot : (Ξ± : Type ?u.7342) β [inst : LE Ξ± Type ?u.7342 β ), ( LinearOrder.toLattice : Lattice β ),
( inferInstance : {Ξ± : Sort ?u.7409} β [i : Ξ± ] β Ξ± : LinearOrder : Type ?u.7408 β Type ?u.7408 β ) with
-- sup := sSup -- Porting note: removed, unnecessary?
-- inf := sInf -- Porting note: removed, unnecessary?
le_csSup := fun s a hb ha β¦ by rw [ sSup_def hb ] ; revert a ha ; exact @ Nat.find_spec _ _ hb
csSup_le := fun s a _ ha β¦ by rw [ sSup_def β¨ a , ha β© ] ; exact Nat.find_min' _ ha
le_csInf := fun s a hs hb β¦ by
rw [ sInf_def hs ] ; exact hb (@ Nat.find_spec ( fun n β¦ n β s ) _ _ : β n , (fun n => n β s ) n )
csInf_le := fun s a _ ha β¦ by rw [ sInf_def β¨ a , ha β© ] ; exact Nat.find_min' _ ha
csSup_empty := by
simp only [ sSup_def , Set.mem_empty_iff_false , forall_const , forall_prop_of_false : β {p : Prop } {q : p β Prop Β¬ p (β (h' : p ), q h' ) β True ) ,
not_false_iff , exists_const ]
apply bot_unique ( Nat.find_min' _ _ )
trivial }
theorem sSup_mem { s : Set β } ( hβ : s . Nonempty ) ( hβ : BddAbove s ) : sSup : {Ξ± : Type ?u.11178} β [self : SupSet Ξ± Set Ξ± Ξ± s β s :=
let β¨ k , hk β© := hβ
hβ . cSup_mem (( finite_le_nat k ). subset hk )
#align nat.Sup_mem Nat.sSup_mem
theorem sInf_add { n : β } { p : β β Prop } ( hn : n β€ sInf : {Ξ± : Type ?u.11367} β [self : InfSet Ξ± Set Ξ± Ξ± { m | p m }) :
sInf : {Ξ± : Type ?u.11398} β [self : InfSet Ξ± Set Ξ± Ξ± { m | p ( m + n ) } + n = sInf : {Ξ± : Type ?u.11451} β [self : InfSet Ξ± Set Ξ± Ξ± { m | p m } := by
obtain h : { m | p (m + n = β
h | β¨ m , hm : m β { m | p (m + n hm β© := { m | p ( m + n ) }. eq_empty_or_nonempty
Β· rw [ h : { m | p (m + n = β
h , Nat.sInf_empty , zero_add ]
obtain hnp : n = sInf { m | p m hnp | hnp : n < sInf { m | p m hnp := hn . eq_or_lt
Β· exact hnp : n = sInf { m | p m hnp
suffices hp : p (sInf { m | p m - n + n hp : p ( sInf : {Ξ± : Type ?u.11824} β [self : InfSet Ξ± Set Ξ± Ξ± { m | p m } - n + n )
Β· exact ( h : { m | p (m + n = β
h . subset : β {Ξ± : Type ?u.11901} {s t : Set Ξ± s = t s β t hp : p (sInf { m | p m - n + n hp ). elim
rw [ tsub_add_cancel_of_le hn ]
exact csInf_mem ( nonempty_of_pos_sInf <| n . zero_le : β (n : β ), 0 β€ n . trans_lt : β {Ξ± : Type ?u.12187} [inst : Preorder Ξ± a b c : Ξ± }, a β€ b b < c a < c hnp : n < sInf { m | p m hnp )
Β· have hp : β n , n β { m | p m hp : β n , n β { m | p m } := β¨ _ , hm : m β { m | p (m + n hm β©
rw [ Nat.sInf_def β¨ m , hm : m β { m | p (m + n hm β©, Nat.sInf_def hp : β n , n β { m | p m hp ]
rw [ Nat.sInf_def hp : β n , n β { m | p m hp ] at hn
exact find_add hn
#align nat.Inf_add Nat.sInf_add
theorem sInf_add' { n : β } { p : β β Prop } ( h : 0 < sInf : {Ξ± : Type ?u.13039} β [self : InfSet Ξ± Set Ξ± Ξ± { m | p m }) :
sInf : {Ξ± : Type ?u.13083} β [self : InfSet Ξ± Set Ξ± Ξ± { m | p m } + n = sInf : {Ξ± : Type ?u.13095} β [self : InfSet Ξ± Set Ξ± Ξ± { m | p ( m - n ) } := by
suffices hβ : n β€ sInf : {Ξ± : Type ?u.13195} β [self : InfSet Ξ± Set Ξ± Ξ± { m | p ( m - n )}
convert sInf_add hβ h.e'_2.h.e'_5.h.e'_3.h.e'_2.h.h.e'_1 hβ
Β· h.e'_2.h.e'_5.h.e'_3.h.e'_2.h.h.e'_1 h.e'_2.h.e'_5.h.e'_3.h.e'_2.h.h.e'_1 hβ simp_rw [ h.e'_2.h.e'_5.h.e'_3.h.e'_2.h.h.e'_1 add_tsub_cancel_right ]
obtain β¨ m , hm β© := nonempty_of_pos_sInf h
refine'
le_csInf β¨ m + n , _ β© fun b hb β¦
le_of_not_lt fun hbn β¦
ne_of_mem_of_not_mem : β {Ξ± : Type ?u.18271} {Ξ² : Type ?u.18272} [inst : Membership Ξ± Ξ² s : Ξ² } {a b : Ξ± }, a β s Β¬ b β s a β b _ ( not_mem_of_lt_sInf h ) ( tsub_eq_zero_of_le hbn . le ) hβ.intro.refine'_1 m + n β { m | p (m - n hβ.intro.refine'_2
Β· hβ.intro.refine'_1 m + n β { m | p (m - n hβ.intro.refine'_1 m + n β { m | p (m - n hβ.intro.refine'_2 dsimp
hβ.intro.refine'_1 m + n β { m | p (m - n rwa [ add_tsub_cancel_right ]
Β· exact hb
#align nat.Inf_add' Nat.sInf_add'
section
variable { Ξ± : Type _ : Type (?u.43343+1)} [ CompleteLattice : Type ?u.43346 β Type ?u.43346 Ξ± ]
theorem iSup_lt_succ : β (u : β β Ξ± n : β ), (β¨ k , β¨ h , u k ) = (β¨ k , β¨ h , u k ) β u n iSup_lt_succ ( u : β β Ξ± ) ( n : β ) : (β¨ k < n + 1 , u k ) = (β¨ k < n , u k ) β u n := by
(β¨ k , β¨ h , u k ) = (β¨ k , β¨ h , u k ) β u n simp [ Nat.lt_succ_iff_lt_or_eq , iSup_or , iSup_sup_eq : β {Ξ± : Type ?u.19113} {ΞΉ : Sort ?u.19114} [inst : CompleteLattice Ξ± f g : ΞΉ β Ξ± (β¨ x , f x β g x ) = (β¨ x , f x ) β β¨ x , g x ]
#align nat.supr_lt_succ Nat.iSup_lt_succ
theorem iSup_lt_succ' ( u : β β Ξ± ) ( n : β ) : (β¨ k < n + 1 , u k ) = u 0 β β¨ k < n , u ( k + 1 ) := by
(β¨ k , β¨ h , u k ) = u 0 β β¨ k , β¨ h , u (k + 1 rw [ (β¨ k , β¨ h , u k ) = u 0 β β¨ k , β¨ h , u (k + 1 β sup_iSup_nat_succ ((β¨ h , u 0 ) β β¨ i , β¨ h , u (i + 1 ) = u 0 β β¨ k , β¨ h , u (k + 1 ] ((β¨ h , u 0 ) β β¨ i , β¨ h , u (i + 1 ) = u 0 β β¨ k , β¨ h , u (k + 1
(β¨ k , β¨ h , u k ) = u 0 β β¨ k , β¨ h , u (k + 1 simp
#align nat.supr_lt_succ' Nat.iSup_lt_succ'
theorem iInf_lt_succ : β (u : β β Ξ± n : β ), (β¨
k , β¨
h , u k ) = (β¨
k , β¨
h , u k ) β u n iInf_lt_succ ( u : β β Ξ± ) ( n : β ) : (β¨
k < n + 1 , u k ) = (β¨
k < n , u k ) β u n :=
@ iSup_lt_succ Ξ± α΅α΅ _ _ _
#align nat.infi_lt_succ Nat.iInf_lt_succ
theorem iInf_lt_succ' ( u : β β Ξ± ) ( n : β ) : (β¨
k < n + 1 , u k ) = u 0 β β¨
k < n , u ( k + 1 ) :=
@ iSup_lt_succ' Ξ± α΅α΅ _ _ _
#align nat.infi_lt_succ' Nat.iInf_lt_succ'
end
end Nat
namespace Set
variable { Ξ± : Type _ : Type (?u.58334+1)}
theorem biUnion_lt_succ ( u : β β Set Ξ± ) ( n : β ) : (β k < n + 1 , u k ) = (β k < n , u k ) βͺ u n :=
Nat.iSup_lt_succ : β {Ξ± : Type ?u.58491} [inst : CompleteLattice Ξ± u : β β Ξ± n : β ), (β¨ k , β¨ h , u k ) = (β¨ k , β¨ h , u k ) β u n u n
#align set.bUnion_lt_succ Set.biUnion_lt_succ
theorem biUnion_lt_succ' ( u : β β Set Ξ± ) ( n : β ) : (β k < n + 1 , u k ) = u 0 βͺ β k < n , u ( k + 1 ) :=
Nat.iSup_lt_succ' : β {Ξ± : Type ?u.58767} [inst : CompleteLattice Ξ± u : β β Ξ± n : β ), (β¨ k , β¨ h , u k ) = u 0 β β¨ k , β¨ h , u (k + 1 u n
#align set.bUnion_lt_succ' Set.biUnion_lt_succ'
theorem biInter_lt_succ ( u : β β Set Ξ± ) ( n : β ) : (β k < n + 1 , u k ) = (β k < n , u k ) β© u n :=
Nat.iInf_lt_succ u n
#align set.bInter_lt_succ Set.biInter_lt_succ
theorem biInter_lt_succ' ( u : β β Set Ξ± ) ( n : β ) : (β k < n + 1 , u k ) = u 0 β© β k < n , u ( k + 1 ) :=
Nat.iInf_lt_succ' u n
#align set.bInter_lt_succ' Set.biInter_lt_succ'
end Set