Conditionally complete linear order structure on ℕ
#
In this file we
- define a
ConditionallyCcompleteLinearOrderBot
structure onℕ
; - prove a few lemmas about
supᵢ
/infᵢ
/Set.unionᵢ
/Set.interᵢ
and natural numbers.
Equations
- Nat.instInfSetNat = { infₛ := fun s => if h : ∃ n, n ∈ s then Nat.find h else 0 }
This instance is necessary, otherwise the lattice operations would be derived via
ConditionallyCompleteLinearOrderBot
and marked as noncomputable.
Equations
- Nat.instLatticeNat = LinearOrder.toLattice
Equations
- One or more equations did not get rendered due to their size.
theorem
Set.bunionᵢ_lt_succ
{α : Type u_1}
(u : ℕ → Set α)
(n : ℕ)
:
(Set.unionᵢ fun k => Set.unionᵢ fun h => u k) = (Set.unionᵢ fun k => Set.unionᵢ fun h => u k) ∪ u n
theorem
Set.bunionᵢ_lt_succ'
{α : Type u_1}
(u : ℕ → Set α)
(n : ℕ)
:
(Set.unionᵢ fun k => Set.unionᵢ fun h => u k) = u 0 ∪ Set.unionᵢ fun k => Set.unionᵢ fun h => u (k + 1)
theorem
Set.binterᵢ_lt_succ
{α : Type u_1}
(u : ℕ → Set α)
(n : ℕ)
:
(Set.interᵢ fun k => Set.interᵢ fun h => u k) = (Set.interᵢ fun k => Set.interᵢ fun h => u k) ∩ u n
theorem
Set.binterᵢ_lt_succ'
{α : Type u_1}
(u : ℕ → Set α)
(n : ℕ)
:
(Set.interᵢ fun k => Set.interᵢ fun h => u k) = u 0 ∩ Set.interᵢ fun k => Set.interᵢ fun h => u (k + 1)