Documentation

BourbakiLean2.Data.Nat.Intervals

@[simp]

theorem Nat.Icc_zero {b : Nat} :

Set.Icc 0 b = Set.Iic b

@[simp]

theorem Nat.Ico_zero {b : Nat} :

Set.Ico 0 b = Set.Iio b

@[simp]

theorem Nat.Ici_zero :

Set.Ici 0 = Set.univ

def Nat.shift {a b : Nat} (c : Nat) :

↥(Set.Icc a b) → ↥(Set.Icc (a + c) (b + c))

Equations

Nat.shift c ⟨x_1, h⟩ = ⟨x_1 + c, ⋯⟩

Instances For

theorem Nat.shift_isOrderIso {a b c : Nat} :

IsOrderIso (Nat.shift c)

def Nat.unshift {a b : Nat} (c : Nat) :

↥(Set.Icc (a + c) (b + c)) → ↥(Set.Icc a b)

Equations

Nat.unshift c ⟨x_1, h⟩ = ⟨x_1 - c, ⋯⟩

Instances For

theorem Nat.shift_inverse_unshift {a b c : Nat} :

Function.IsInverseOf (Nat.shift c) (Nat.unshift c)

theorem Nat.unshift_isOrderIso {a b c : Nat} :

IsOrderIso (Nat.unshift c)

@[simp]

theorem Nat.shift_unshift_val {a b c : Nat} {d : ↥(Set.Icc a b)} :

Nat.unshift c (Nat.shift c d) = d

@[simp]

theorem Nat.unshift_shift_val {a b c : Nat} {d : ↥(Set.Icc (a + c) (b + c))} :

Nat.shift c (Nat.unshift c d) = d

@[simp]

theorem Nat.shift_zero {a b : Nat} :

Nat.shift 0 = id

@[simp]

theorem Nat.unshift_zero {a b : Nat} :

Nat.unshift 0 = id

instance Nat.Iic_finite {a : Nat} :

Finite ↥(Set.Iic a)

Equations

⋯ = ⋯

instance Nat.Icc_finite {a b : Nat} :

Finite ↥(Set.Icc a b)

Equations

⋯ = ⋯

@[simp]

theorem Nat.Iio_succ {a : Nat} :

Set.Iio (a + 1) = Set.Iic a

@[simp]

theorem Nat.Ioi_eq_Ici_succ {a : Nat} :

Set.Ioi a = Set.Ici (a + 1)

@[simp]

theorem Nat.Ioo_eq_Ico_succ {a b : Nat} :

Set.Ioo a b = Set.Ico (a + 1) b

@[simp]

theorem Nat.Ico_succ {a b : Nat} :

Set.Ico a (b + 1) = Set.Icc a b

@[simp]

theorem Nat.Ioc_eq_Icc_succ {a b : Nat} :

Set.Ioc a b = Set.Icc (a + 1) b

instance Nat.Iio_finite {a : Nat} :

Finite ↥(Set.Iio a)

Equations

⋯ = ⋯

instance Nat.Ico_finite {a b : Nat} :

Finite ↥(Set.Ico a b)

Equations

⋯ = ⋯

instance Nat.Ioo_finite {a b : Nat} :

Finite ↥(Set.Ioo a b)

Equations

⋯ = ⋯

instance Nat.Ioc_finite {a b : Nat} :

Finite ↥(Set.Ioc a b)

Equations

⋯ = ⋯

@[simp]

theorem Nat.Iic_cardinality {a : Nat} :

(Finite.ftype ↥(Set.Iic a)).cardinality = a + 1

@[simp]

theorem Nat.Iio_cardinality {a : Nat} :

(Finite.ftype ↥(Set.Iio a)).cardinality = a

@[simp]

theorem Nat.Icc_cardinality {a b : Nat} (h : a ≤ b) :

(Finite.ftype ↥(Set.Icc a b)).cardinality = b - a + 1

@[simp]

theorem Nat.Ioc_cardinality {a b : Nat} :

(Finite.ftype ↥(Set.Ioc a b)).cardinality = b - a

@[simp]

theorem Nat.Ico_cardinality {a b : Nat} :

(Finite.ftype ↥(Set.Ico a b)).cardinality = b - a

@[simp]

theorem Nat.Ioo_cardinality {a b : Nat} :

(Finite.ftype ↥(Set.Ioo a b)).cardinality = b - a - 1

theorem Nat.mem_Iio_2 {a : Nat} :

a ∈ Set.Iio 2 ↔ a = 0 ∨ a = 1

theorem Nat.lt_Iio_2 {a b : Nat} (h : a ∈ Set.Iio 2) (h' : b ∈ Set.Iio 2) (h'' : a < b) :

a = 0 ∧ b = 1

theorem Finite.equipotent_Iio {α : Type u_1} [Finite α] :

Equipotent α ↥(Set.Iio (Finite.ftype α).cardinality)

theorem TotalOrder.exists_iso_interval {α : Type u_1} [TotalOrder α] [Finite α] :

∃ (f : α → ↥(Set.Iio (Finite.ftype α).cardinality)), IsOrderIso f

theorem TotalOrder.ex_unique_iso_interval {α : Type u_1} [TotalOrder α] [Finite α] :

∃! f : α → ↥(Set.Iio (Finite.ftype α).cardinality), IsOrderIso f

noncomputable def TotalOrder.enumerate {α : Type u_1} [TotalOrder α] [Finite α] :

α → ↥(Set.Iio (Finite.ftype α).cardinality)

Equations

TotalOrder.enumerate = ⋯.choose

Instances For

@[simp]

theorem TotalOrder.enumerate_isOrderIso {α : Type u_1} [TotalOrder α] [Finite α] :

IsOrderIso TotalOrder.enumerate

noncomputable def TotalOrder.nth {α : Type u_1} [TotalOrder α] [Finite α] :

↥(Set.Iio (Finite.ftype α).cardinality) → α

Equations

TotalOrder.nth = ⋯.inv

Instances For

noncomputable def TotalOrder.nth_isOrderIso {α : Type u_1} [TotalOrder α] [Finite α] :

IsOrderIso TotalOrder.nth

Equations

⋯ = ⋯

Instances For

@[simp]

theorem TotalOrder.enumerate_nth {α : Type u_1} [TotalOrder α] [Finite α] {a : ↥(Set.Iio (Finite.ftype α).cardinality)} :

TotalOrder.enumerate (TotalOrder.nth a) = a

@[simp]

theorem TotalOrder.nth_enumerate {α : Type u_1} [TotalOrder α] [Finite α] {a : α} :

TotalOrder.nth (TotalOrder.enumerate a) = a

@[simp]

theorem TotalOrder.nth_le_iff {α : Type u_1} [TotalOrder α] [Finite α] {x y : ↥(Set.Iio (Finite.ftype α).cardinality)} :

TotalOrder.nth x ≤ TotalOrder.nth y ↔ x ≤ y

@[simp]

theorem TotalOrder.nth_lt_iff {α : Type u_1} [TotalOrder α] [Finite α] {x y : ↥(Set.Iio (Finite.ftype α).cardinality)} :

TotalOrder.nth x < TotalOrder.nth y ↔ x < y

@[simp]

theorem TotalOrder.enumerate_le_iff {α : Type u_1} [TotalOrder α] [Finite α] {x y : α} :

TotalOrder.enumerate x ≤ TotalOrder.enumerate y ↔ x ≤ y

@[simp]

theorem TotalOrder.enumerate_lt_iff {α : Type u_1} [TotalOrder α] [Finite α] {x y : α} :

TotalOrder.enumerate x < TotalOrder.enumerate y ↔ x < y

@[simp]

theorem TotalOrder.nth_zero {α : Type u_1} [TotalOrder α] [Finite α] [Nonempty α] :

TotalOrder.nth ⟨0, ⋯⟩ = ⊥

@[simp]

theorem TotalOrder.enumerate_least {α : Type u_1} [TotalOrder α] [Finite α] [Nonempty α] :

TotalOrder.enumerate ⊥ = ⟨0, ⋯⟩