Conditionally complete linear order structure on ℕ
#
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we
- define a
conditionally_complete_linear_order_bot
structure onℕ
; - prove a few lemmas about
supr
/infi
/set.Union
/set.Inter
and natural numbers.
@[protected, instance]
This instance is necessary, otherwise the lattice operations would be derived via conditionally_complete_linear_order_bot and marked as noncomputable.
Equations
@[protected, instance]
Equations
- nat.conditionally_complete_linear_order_bot = {sup := lattice.sup linear_order.to_lattice, le := lattice.le linear_order.to_lattice, lt := lattice.lt linear_order.to_lattice, le_refl := nat.conditionally_complete_linear_order_bot._proof_1, le_trans := nat.conditionally_complete_linear_order_bot._proof_2, lt_iff_le_not_le := nat.conditionally_complete_linear_order_bot._proof_3, le_antisymm := nat.conditionally_complete_linear_order_bot._proof_4, le_sup_left := nat.conditionally_complete_linear_order_bot._proof_5, le_sup_right := nat.conditionally_complete_linear_order_bot._proof_6, sup_le := nat.conditionally_complete_linear_order_bot._proof_7, inf := lattice.inf linear_order.to_lattice, inf_le_left := nat.conditionally_complete_linear_order_bot._proof_8, inf_le_right := nat.conditionally_complete_linear_order_bot._proof_9, le_inf := nat.conditionally_complete_linear_order_bot._proof_10, Sup := has_Sup.Sup nat.has_Sup, Inf := has_Inf.Inf nat.has_Inf, le_cSup := nat.conditionally_complete_linear_order_bot._proof_11, cSup_le := nat.conditionally_complete_linear_order_bot._proof_12, cInf_le := nat.conditionally_complete_linear_order_bot._proof_13, le_cInf := nat.conditionally_complete_linear_order_bot._proof_14, le_total := nat.conditionally_complete_linear_order_bot._proof_15, decidable_le := linear_order.decidable_le infer_instance, decidable_eq := linear_order.decidable_eq infer_instance, decidable_lt := linear_order.decidable_lt infer_instance, max_def := nat.conditionally_complete_linear_order_bot._proof_16, min_def := nat.conditionally_complete_linear_order_bot._proof_17, bot := order_bot.bot infer_instance, bot_le := nat.conditionally_complete_linear_order_bot._proof_18, cSup_empty := nat.conditionally_complete_linear_order_bot._proof_19}
theorem
nat.Inf_add
{n : ℕ}
{p : ℕ → Prop}
(hn : n ≤ has_Inf.Inf {m : ℕ | p m}) :
has_Inf.Inf {m : ℕ | p (m + n)} + n = has_Inf.Inf {m : ℕ | p m}
theorem
nat.Inf_add'
{n : ℕ}
{p : ℕ → Prop}
(h : 0 < has_Inf.Inf {m : ℕ | p m}) :
has_Inf.Inf {m : ℕ | p m} + n = has_Inf.Inf {m : ℕ | p (m - n)}