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) 2021 YaΓ«l Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: YaΓ«l Dillies
! This file was ported from Lean 3 source module data.int.interval
! leanprover-community/mathlib commit f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.CharZero.Lemmas
import Mathlib.Order.LocallyFinite
import Mathlib.Data.Finset.LocallyFinite
/-!
# Finite intervals of integers
This file proves that `β€` is a `LocallyFiniteOrder` and calculates the cardinality of its
intervals as finsets and fintypes.
-/
open Finset Int
instance : LocallyFiniteOrder β€
where
finsetIcc a b :=
( Finset.range ( b + 1 - a ). toNat ). map <| Nat.castEmbedding . trans : {Ξ± : Sort ?u.231} β {Ξ² : Sort ?u.230} β {Ξ³ : Sort ?u.229} β (Ξ± βͺ Ξ² (Ξ² βͺ Ξ³ Ξ± βͺ Ξ³ <| addLeftEmbedding a
finsetIco a b := ( Finset.range ( b - a ). toNat ). map <| Nat.castEmbedding . trans : {Ξ± : Sort ?u.479} β {Ξ² : Sort ?u.478} β {Ξ³ : Sort ?u.477} β (Ξ± βͺ Ξ² (Ξ² βͺ Ξ³ Ξ± βͺ Ξ³ <| addLeftEmbedding a
finsetIoc a b :=
( Finset.range ( b - a ). toNat ). map <| Nat.castEmbedding . trans : {Ξ± : Sort ?u.587} β {Ξ² : Sort ?u.586} β {Ξ³ : Sort ?u.585} β (Ξ± βͺ Ξ² (Ξ² βͺ Ξ³ Ξ± βͺ Ξ³ <| addLeftEmbedding ( a + 1 )
finsetIoo a b :=
( Finset.range ( b - a - 1 ). toNat ). map <| Nat.castEmbedding . trans : {Ξ± : Sort ?u.783} β {Ξ² : Sort ?u.782} β {Ξ³ : Sort ?u.781} β (Ξ± βͺ Ξ² (Ξ² βͺ Ξ³ Ξ± βͺ Ξ³ <| addLeftEmbedding ( a + 1 )
finset_mem_Icc a b x := by
simp_rw [ mem_map , mem_range , Int.lt_toNat , Function.Embedding.trans_apply ,
Nat.castEmbedding_apply , addLeftEmbedding_apply ]
constructor
Β· rintro β¨a, h, rflβ© : βa < b + 1 - aβ β§ aβ + βa = x a β¨a, h, rflβ© : βa < b + 1 - aβ β§ aβ + βa = x h β¨a, h, rflβ© : βa < b + 1 - aβ β§ aβ + βa = x rfl β¨a, h, rflβ© : βa < b + 1 - aβ β§ aβ + βa = x
rw [ lt_sub_iff_add_lt , Int.lt_add_one_iff : β {a b : β€ }, a < b + 1 β a β€ b , add_comm ] at h
exact β¨ Int.le.intro : β {a b : β€ } (n : β ), a + βn = b a β€ b a rfl : β {Ξ± : Sort ?u.3411} {a : Ξ± }, a = a , h β©
Β· rintro β¨ ha , hb β© mpr.intro β a_1 , βa_1 < b + 1 - a β§ a + βa_1 = x
use ( x - a ). toNat
rw [ β lt_add_one_iff ] at hb
rw [ toNat_sub_of_le : β {a b : β€ }, b β€ a β(toNat (a - b = a - b ha ]
exact β¨ sub_lt_sub_right hb _ , add_sub_cancel'_right : β {G : Type ?u.3583} [inst : AddCommGroup G a b : G ), a + (b - a = b _ _ β©
finset_mem_Ico a b x := by
simp_rw [ mem_map , mem_range , Int.lt_toNat , Function.Embedding.trans_apply ,
Nat.castEmbedding_apply , addLeftEmbedding_apply ]
constructor
Β· rintro β¨ a , h , rfl β©
exact β¨ Int.le.intro : β {a b : β€ } (n : β ), a + βn = b a β€ b a rfl : β {Ξ± : Sort ?u.4444} {a : Ξ± }, a = a , lt_sub_iff_add_lt' . mp : β {a b : Prop }, (a β b a β b h β©
Β· rintro β¨ ha , hb β© mpr.intro β a_1 , βa_1 < b - a β§ a + βa_1 = x
use ( x - a ). toNat
rw [ toNat_sub_of_le : β {a b : β€ }, b β€ a β(toNat (a - b = a - b ha ]
exact β¨ sub_lt_sub_right hb _ , add_sub_cancel'_right : β {G : Type ?u.4702} [inst : AddCommGroup G a b : G ), a + (b - a = b _ _ β©
finset_mem_Ioc a b x := by
simp_rw [ mem_map , mem_range , Int.lt_toNat , Function.Embedding.trans_apply ,
Nat.castEmbedding_apply , addLeftEmbedding_apply ]
constructor
Β· rintro β¨a, h, rflβ© : βa < b - aβ β§ aβ + 1 + βa = x a β¨a, h, rflβ© : βa < b - aβ β§ aβ + 1 + βa = x h β¨a, h, rflβ© : βa < b - aβ β§ aβ + 1 + βa = x rfl β¨a, h, rflβ© : βa < b - aβ β§ aβ + 1 + βa = x
rw [ β add_one_le_iff , le_sub_iff_add_le' , add_comm _ ( 1 : β€ ), β add_assoc ] at h
exact β¨ Int.le.intro : β {a b : β€ } (n : β ), a + βn = b a β€ b a rfl : β {Ξ± : Sort ?u.5761} {a : Ξ± }, a = a , h β©
Β· rintro β¨ ha , hb β© mpr.intro β a_1 , βa_1 < b - a β§ a + 1 + βa_1 = x
use ( x - ( a + 1 )). toNat
rw [ toNat_sub_of_le : β {a b : β€ }, b β€ a β(toNat (a - b = a - b ha , β add_one_le_iff , sub_add , add_sub_cancel : β {G : Type ?u.5938} [inst : AddGroup G a b : G ), a + b - b = a ]
exact β¨ sub_le_sub_right hb _ , add_sub_cancel'_right : β {G : Type ?u.6080} [inst : AddCommGroup G a b : G ), a + (b - a = b _ _ β©
finset_mem_Ioo a b x := by
simp_rw [ mem_map , mem_range , Int.lt_toNat , Function.Embedding.trans_apply ,
Nat.castEmbedding_apply , addLeftEmbedding_apply ]
constructor mp (β a_1 , βa_1 < b - a - 1 β§ a + 1 + βa_1 = x ) β a < x β§ x < b mpr a < x β§ x < b β a_2 , βa_2 < b - a - 1 β§ a + 1 + βa_2 = x
Β· mp (β a_1 , βa_1 < b - a - 1 β§ a + 1 + βa_1 = x ) β a < x β§ x < b mp (β a_1 , βa_1 < b - a - 1 β§ a + 1 + βa_1 = x ) β a < x β§ x < b mpr a < x β§ x < b β a_2 , βa_2 < b - a - 1 β§ a + 1 + βa_2 = x rintro β¨ a , h , rfl β© mp.intro.intro aβ < aβ + 1 + βa β§ aβ + 1 + βa < b
mp (β a_1 , βa_1 < b - a - 1 β§ a + 1 + βa_1 = x ) β a < x β§ x < b rw [ mp.intro.intro aβ < aβ + 1 + βa β§ aβ + 1 + βa < b sub_sub , mp.intro.intro aβ < aβ + 1 + βa β§ aβ + 1 + βa < b mp.intro.intro aβ < aβ + 1 + βa β§ aβ + 1 + βa < b lt_sub_iff_add_lt' mp.intro.intro aβ < aβ + 1 + βa β§ aβ + 1 + βa < b ] mp.intro.intro aβ < aβ + 1 + βa β§ aβ + 1 + βa < b at h mp.intro.intro aβ < aβ + 1 + βa β§ aβ + 1 + βa < b
mp (β a_1 , βa_1 < b - a - 1 β§ a + 1 + βa_1 = x ) β a < x β§ x < b exact β¨ Int.le.intro : β {a b : β€ } (n : β ), a + βn = b a β€ b a rfl : β {Ξ± : Sort ?u.7079} {a : Ξ± }, a = a , h β©
Β· mpr a < x β§ x < b β a_2 , βa_2 < b - a - 1 β§ a + 1 + βa_2 = x mpr a < x β§ x < b β a_2 , βa_2 < b - a - 1 β§ a + 1 + βa_2 = x rintro β¨ ha , hb β© a, b, x : β€ ha : a < x hb : x < b mpr.intro β a_1 , βa_1 < b - a - 1 β§ a + 1 + βa_1 = x
mpr a < x β§ x < b β a_2 , βa_2 < b - a - 1 β§ a + 1 + βa_2 = x use ( x - ( a + 1 )). toNat a, b, x : β€ ha : a < x hb : x < b mpr.intro
mpr a < x β§ x < b β a_2 , βa_2 < b - a - 1 β§ a + 1 + βa_2 = x rw [ a, b, x : β€ ha : a < x hb : x < b mpr.intro toNat_sub_of_le : β {a b : β€ }, b β€ a β(toNat (a - b = a - b ha , a, b, x : β€ ha : a < x hb : x < b mpr.intro a, b, x : β€ ha : a < x hb : x < b mpr.intro sub_sub a, b, x : β€ ha : a < x hb : x < b mpr.intro ] a, b, x : β€ ha : a < x hb : x < b mpr.intro
mpr a < x β§ x < b β a_2 , βa_2 < b - a - 1 β§ a + 1 + βa_2 = x exact β¨ sub_lt_sub_right hb _ , add_sub_cancel'_right : β {G : Type ?u.7262} [inst : AddCommGroup G a b : G ), a + (b - a = b _ _ β©
namespace Int
variable ( a b : β€ )
theorem Icc_eq_finset_map :
Icc a b =
( Finset.range ( b + 1 - a ). toNat ). map ( Nat.castEmbedding . trans : {Ξ± : Sort ?u.9484} β {Ξ² : Sort ?u.9483} β {Ξ³ : Sort ?u.9482} β (Ξ± βͺ Ξ² (Ξ² βͺ Ξ³ Ξ± βͺ Ξ³ <| addLeftEmbedding a ) :=
rfl : β {Ξ± : Sort ?u.9648} {a : Ξ± }, a = a
#align int.Icc_eq_finset_map Int.Icc_eq_finset_map
theorem Ico_eq_finset_map :
Ico a b = ( Finset.range ( b - a ). toNat ). map ( Nat.castEmbedding . trans : {Ξ± : Sort ?u.9839} β {Ξ² : Sort ?u.9838} β {Ξ³ : Sort ?u.9837} β (Ξ± βͺ Ξ² (Ξ² βͺ Ξ³ Ξ± βͺ Ξ³ <| addLeftEmbedding a ) :=
rfl : β {Ξ± : Sort ?u.9995} {a : Ξ± }, a = a
#align int.Ico_eq_finset_map Int.Ico_eq_finset_map
theorem Ioc_eq_finset_map :
Ioc a b =
( Finset.range ( b - a ). toNat ). map ( Nat.castEmbedding . trans : {Ξ± : Sort ?u.10186} β {Ξ² : Sort ?u.10185} β {Ξ³ : Sort ?u.10184} β (Ξ± βͺ Ξ² (Ξ² βͺ Ξ³ Ξ± βͺ Ξ³ <| addLeftEmbedding ( a + 1 )) :=
rfl : β {Ξ± : Sort ?u.10428} {a : Ξ± }, a = a
#align int.Ioc_eq_finset_map Int.Ioc_eq_finset_map
theorem Ioo_eq_finset_map :
Ioo a b =
( Finset.range ( b - a - 1 ). toNat ). map ( Nat.castEmbedding . trans : {Ξ± : Sort ?u.10660} β {Ξ² : Sort ?u.10659} β {Ξ³ : Sort ?u.10658} β (Ξ± βͺ Ξ² (Ξ² βͺ Ξ³ Ξ± βͺ Ξ³ <| addLeftEmbedding ( a + 1 )) :=
rfl : β {Ξ± : Sort ?u.10926} {a : Ξ± }, a = a
#align int.Ioo_eq_finset_map Int.Ioo_eq_finset_map
@[ simp ]
theorem card_Icc : ( Icc a b ). card = ( b + 1 - a ). toNat := by
change ( Finset.map _ _ ). card = _
rw [ Finset.card_map , Finset.card_range ]
#align int.card_Icc Int.card_Icc
@[ simp ]
theorem card_Ico : ( Ico a b ). card = ( b - a ). toNat := by
change ( Finset.map _ _ ). card = _
rw [ Finset.card_map , Finset.card_range ]
#align int.card_Ico Int.card_Ico
@[ simp ]
theorem card_Ioc : ( Ioc a b ). card = ( b - a ). toNat := by
change ( Finset.map _ _ ). card = _
rw [ Finset.card_map , Finset.card_range ]
#align int.card_Ioc Int.card_Ioc
@[ simp ]
theorem card_Ioo : ( Ioo a b ). card = ( b - a - 1 ). toNat := by
change ( Finset.map _ _ ). card = _
rw [ Finset.card_map , Finset.card_range ]
#align int.card_Ioo Int.card_Ioo
theorem card_Icc_of_le ( h : a β€ b + 1 ) : (( Icc a b ). card : β€ ) = b + 1 - a := by
rw [ card_Icc , toNat_sub_of_le : β {a b : β€ }, b β€ a β(toNat (a - b = a - b h ]
#align int.card_Icc_of_le Int.card_Icc_of_le
theorem card_Ico_of_le ( h : a β€ b ) : (( Ico a b ). card : β€ ) = b - a := by
rw [ card_Ico , toNat_sub_of_le : β {a b : β€ }, b β€ a β(toNat (a - b = a - b h ]
#align int.card_Ico_of_le Int.card_Ico_of_le : β (a b : β€ ), a β€ b β(card (Ico a b = b - a
theorem card_Ioc_of_le ( h : a β€ b ) : (( Ioc a b ). card : β€ ) = b - a := by
rw [ card_Ioc , toNat_sub_of_le : β {a b : β€ }, b β€ a β(toNat (a - b = a - b h ]
#align int.card_Ioc_of_le Int.card_Ioc_of_le : β (a b : β€ ), a β€ b β(card (Ioc a b = b - a
theorem card_Ioo_of_lt : a < b β(card (Ioo a b = b - a - 1 card_Ioo_of_lt ( h : a < b ) : (( Ioo a b ). card : β€ ) = b - a - 1 := by
rw [ card_Ioo , sub_sub , toNat_sub_of_le : β {a b : β€ }, b β€ a β(toNat (a - b = a - b h b - (a + 1 = b - (a + 1 ]
#align int.card_Ioo_of_lt Int.card_Ioo_of_lt : β (a b : β€ ), a < b β(card (Ioo a b = b - a - 1
-- porting note: removed `simp` attribute because `simpNF` says it can prove it
theorem card_fintype_Icc : Fintype.card ( Set.Icc : {Ξ± : Type ?u.13149} β [inst : Preorder Ξ± Ξ± β Ξ± β Set Ξ± a b ) = ( b + 1 - a ). toNat := by
rw [ β card_Icc , Fintype.card_ofFinset ]
#align int.card_fintype_Icc Int.card_fintype_Icc
-- porting note: removed `simp` attribute because `simpNF` says it can prove it
theorem card_fintype_Ico : Fintype.card ( Set.Ico : {Ξ± : Type ?u.13678} β [inst : Preorder Ξ± Ξ± β Ξ± β Set Ξ± a b ) = ( b - a ). toNat := by
rw [ β card_Ico , Fintype.card_ofFinset ]
#align int.card_fintype_Ico Int.card_fintype_Ico
-- porting note: removed `simp` attribute because `simpNF` says it can prove it
theorem card_fintype_Ioc : Fintype.card ( Set.Ioc : {Ξ± : Type ?u.14131} β [inst : Preorder Ξ± Ξ± β Ξ± β Set Ξ± a b ) = ( b - a ). toNat := by
rw [ β card_Ioc , Fintype.card_ofFinset ]
#align int.card_fintype_Ioc Int.card_fintype_Ioc
-- porting note: removed `simp` attribute because `simpNF` says it can prove it
theorem card_fintype_Ioo : Fintype.card ( Set.Ioo : {Ξ± : Type ?u.14578} β [inst : Preorder Ξ± Ξ± β Ξ± β Set Ξ± a b ) = ( b - a - 1 ). toNat := by
rw [ β card_Ioo , Fintype.card_ofFinset ]
#align int.card_fintype_Ioo Int.card_fintype_Ioo
theorem card_fintype_Icc_of_le ( h : a β€ b + 1 ) : ( Fintype.card ( Set.Icc : {Ξ± : Type ?u.15141} β [inst : Preorder Ξ± Ξ± β Ξ± β Set Ξ± a b ) : β€ ) = b + 1 - a := by
rw [ card_fintype_Icc , toNat_sub_of_le : β {a b : β€ }, b β€ a β(toNat (a - b = a - b h ]
#align int.card_fintype_Icc_of_le Int.card_fintype_Icc_of_le
theorem card_fintype_Ico_of_le ( h : a β€ b ) : ( Fintype.card ( Set.Ico : {Ξ± : Type ?u.15681} β [inst : Preorder Ξ± Ξ± β Ξ± β Set Ξ± a b ) : β€ ) = b - a := by
rw [ card_fintype_Ico , toNat_sub_of_le : β {a b : β€ }, b β€ a β(toNat (a - b = a - b h ]
#align int.card_fintype_Ico_of_le Int.card_fintype_Ico_of_le
theorem card_fintype_Ioc_of_le ( h : a β€ b ) : ( Fintype.card ( Set.Ioc : {Ξ± : Type ?u.16175} β [inst : Preorder Ξ± Ξ± β Ξ± β Set Ξ± a b ) : β€ ) = b - a := by
rw [ card_fintype_Ioc , toNat_sub_of_le : β {a b : β€ }, b β€ a β(toNat (a - b = a - b h ]
#align int.card_fintype_Ioc_of_le Int.card_fintype_Ioc_of_le
theorem card_fintype_Ioo_of_lt ( h : a < b ) : ( Fintype.card ( Set.Ioo : {Ξ± : Type ?u.16663} β [inst : Preorder Ξ± Ξ± β Ξ± β Set Ξ± a b ) : β€ ) = b - a - 1 := by
rw [ card_fintype_Ioo , sub_sub , toNat_sub_of_le : β {a b : β€ }, b β€ a β(toNat (a - b = a - b h b - (a + 1 = b - (a + 1 ]
#align int.card_fintype_Ioo_of_lt Int.card_fintype_Ioo_of_lt
theorem image_Ico_emod ( n a : β€ ) ( h : 0 β€ a ) : ( Ico n ( n + a )). image (Β· % a ) = Ico 0 a := by
obtain rfl rfl | ha : 0 = a β¨ 0 < a ha := eq_or_lt_of_le h inl aβ, b, n, a : β€ h : 0 β€ a ha : 0 < a inr
Β· inl aβ, b, n, a : β€ h : 0 β€ a ha : 0 < a inr simp
ext i
simp only [ mem_image , mem_range , mem_Ico ]
constructor
Β· rintro β¨ i , _ , rfl β©
exact β¨ emod_nonneg : β (a : β€ ) {b : β€ }, b β 0 0 β€ a % b i ha . ne' : β {Ξ± : Type ?u.18973} [inst : Preorder Ξ± x y : Ξ± }, x < y y β x , emod_lt_of_pos : β (a : β€ ) {b : β€ }, 0 < b a % b < b i ha β©
intro hia
have hn := Int.emod_add_ediv : β (a b : β€ ), a % b + b * (a / b = a n a
obtain hi | hi := lt_or_le i ( n % a ) inr.a.mpr.inl inr.a.mpr.inr
Β· inr.a.mpr.inl inr.a.mpr.inr refine' β¨ i + a * ( n / a + 1 ), β¨ _ , _ β©, _ β© inr.a.mpr.inl.refine'_1 inr.a.mpr.inl.refine'_2 inr.a.mpr.inl.refine'_3
Β·