theorem ENat.eq_zero_or_exists_eq_add_one (a : ℕ∞) : a = 0 ∨ ∃ (i : ℕ∞), a = i + 1

def ENat.recTopZeroCoe {C : ℕ∞ → Sort u_1} (top : C ⊤) (zero : C 0) (coe : (a : ℕ) → C ↑(a + 1)) (n : ℕ∞) : C n

Equations

• One or more equations did not get rendered due to their size.

theorem ENat.recZeroSucc {C : ℕ∞ → Prop} (zero : C 0) (coe : ∀ (a : ℕ∞), C (a + 1)) (n : ℕ∞) : C n

theorem ENat.nat_induction' {motive : ℕ∞ → Prop} (a : ℕ∞) (zero : motive 0) (succ : ∀ n < ⊤, motive n → motive (n + 1)) (top : (∀ n < ⊤, motive n) → motive ⊤) : motive a

A version of ENat.nat_induction' which stays in the type ℕ∞.

theorem ENat.add_ne_top {x y : ℕ∞} : x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

theorem ENat.top_mul_eq_ite (a : ℕ∞) : ⊤ * a = if a = 0 then 0 else ⊤

theorem ENat.mul_top_eq_ite (a : ℕ∞) : a * ⊤ = if a = 0 then 0 else ⊤

@[simp]

theorem ENat.ofNat_lt_top {n : ℕ} [n.AtLeastTwo] : OfNat.ofNat n < ⊤

@[simp]

theorem ENat.ofNat_le_ofNat {m n : ℕ} [m.AtLeastTwo] [n.AtLeastTwo] : OfNat.ofNat m ≤ OfNat.ofNat n ↔ m ≤ n

@[simp]

theorem ENat.ofNat_lt_ofNat {m n : ℕ} [m.AtLeastTwo] [n.AtLeastTwo] : OfNat.ofNat m < OfNat.ofNat n ↔ m < n

@[simp]

theorem ENat.ofNat_inj {m n : ℕ} [m.AtLeastTwo] [n.AtLeastTwo] : OfNat.ofNat m = OfNat.ofNat n ↔ m = n

@[simp]

theorem ENat.one_lt_ofNat {n : ℕ} [n.AtLeastTwo] : 1 < OfNat.ofNat n

@[simp]

theorem ENat.zero_lt_ofNat {n : ℕ} [n.AtLeastTwo] : 0 < OfNat.ofNat n

@[simp]

theorem ENat.one_le_ofNat {n : ℕ} [n.AtLeastTwo] : 1 ≤ OfNat.ofNat n

@[simp]

theorem ENat.not_ofNat_le_one {n : ℕ} [n.AtLeastTwo] : ¬OfNat.ofNat n ≤ 1

theorem ENat.coe_eq_ofNat {n : ℕ} [n.AtLeastTwo] : ↑n = OfNat.ofNat n

@[simp]

theorem ENat.coe_le_ofNat {m n : ℕ} [n.AtLeastTwo] : ↑m ≤ OfNat.ofNat n ↔ m ≤ n

@[simp]

theorem ENat.coe_lt_ofNat {m n : ℕ} [n.AtLeastTwo] : ↑m < OfNat.ofNat n ↔ m < n

@[simp]

theorem ENat.ofNat_le_coe {m n : ℕ} [m.AtLeastTwo] : OfNat.ofNat m ≤ ↑n ↔ m ≤ n

@[simp]

theorem ENat.ofNat_lt_coe {m n : ℕ} [m.AtLeastTwo] : OfNat.ofNat m < ↑n ↔ m < n

@[simp]

theorem ENat.coe_eq_ofNat_iff {m n : ℕ} [n.AtLeastTwo] : ↑m = OfNat.ofNat n ↔ m = n

@[simp]

theorem ENat.zero_le {n : ℕ∞} : 0 ≤ n

@[simp]

theorem ENat.ofNat_ne_zero {n : ℕ} [n.AtLeastTwo] : OfNat.ofNat n ≠ 0

theorem ENat.top_mul_ofNat {n : ℕ} [n.AtLeastTwo] : ⊤ * OfNat.ofNat n = ⊤

@[simp]

theorem ENat.tsub_add_cancel_iff_le {a b : ℕ∞} : b - a + a = b ↔ a ≤ b

theorem ENat.add_tsub_cancel {a b : ℕ∞} (hab : a ≤ b) (hb : b ≠ ⊤) : a + b - a = b

theorem ENat.add_tsub_cancel_right {a b : ℕ∞} (hb : b ≠ ⊤) : a + b - b = a

@[simp]

theorem ENat.one_le_two : 1 ≤ 2

@[simp]

theorem ENat.coe_eq_zero (a : ℕ) : ↑a = 0 ↔ a = 0

theorem ENat.mul_eq_top_iff {a b : ℕ∞} : a * b = ⊤ ↔ a = ⊤ ∧ b ≠ 0 ∨ a ≠ 0 ∧ b = ⊤

@[simp]

theorem ENat.ofNat_mul_eq_top_iff {n : ℕ} [n.AtLeastTwo] {a : ℕ∞} : OfNat.ofNat n * a = ⊤ ↔ a = ⊤

@[simp]

theorem ENat.mul_ofNat_eq_top_iff {n : ℕ} [n.AtLeastTwo] {a : ℕ∞} : a * OfNat.ofNat n = ⊤ ↔ a = ⊤

@[simp]

theorem ENat.coe_mul_eq_top_iff {n : ℕ} {a : ℕ∞} : a * ↑n = ⊤ ↔ a = ⊤ ∧ n ≠ 0

@[simp]

theorem ENat.mul_coe_eq_top_iff {n : ℕ} {a : ℕ∞} : ↑n * a = ⊤ ↔ a = ⊤ ∧ n ≠ 0

@[simp]

theorem ENat.add_eq_left_iff {a b : ℕ∞} : a + b = a ↔ a = ⊤ ∨ b = 0

@[simp]

theorem ENat.add_eq_right_iff {a b : ℕ∞} : a + b = b ↔ a = 0 ∨ b = ⊤

@[simp]

theorem ENat.eq_add_right_iff {a b : ℕ∞} : b = a + b ↔ a = 0 ∨ b = ⊤

@[simp]

theorem ENat.eq_add_left_iff {a b : ℕ∞} : a = a + b ↔ b = 0 ∨ a = ⊤

@[simp]

theorem ENat.add_le_left_iff {a b : ℕ∞} : a + b ≤ a ↔ a = ⊤ ∨ b = 0

@[simp]

theorem ENat.add_le_right_iff {a b : ℕ∞} : a + b ≤ b ↔ a = 0 ∨ b = ⊤

@[simp]

theorem ENat.add_one_le_add_one_iff {a b : ℕ∞} : a + 1 ≤ b + 1 ↔ a ≤ b

@[simp]

theorem ENat.one_add_le_one_add_iff {a b : ℕ∞} : 1 + a ≤ 1 + b ↔ a ≤ b

@[simp]

theorem ENat.add_one_lt_add_one_iff {a b : ℕ∞} : a + 1 < b + 1 ↔ a < b

@[simp]

theorem ENat.one_add_lt_one_add_iff {a b : ℕ∞} : 1 + a < 1 + b ↔ a < b

@[simp]

theorem ENat.add_one_inj {a b : ℕ∞} : a + 1 = b + 1 ↔ a = b

@[simp]

theorem ENat.one_add_inj {a b : ℕ∞} : 1 + a = 1 + b ↔ a = b

@[simp]

theorem ENat.eq_left_add_iff {a b : ℕ∞} : a = a + b ↔ a = ⊤ ∨ b = 0

@[simp]

theorem ENat.eq_right_add_iff {a b : ℕ∞} : b = a + b ↔ b = ⊤ ∨ a = 0

@[simp]

theorem ENat.lt_add_left_iff {a b : ℕ∞} : a < a + b ↔ a ≠ ⊤ ∧ b ≠ 0

@[simp]

theorem ENat.lt_add_right_iff {a b : ℕ∞} : a < b + a ↔ a ≠ ⊤ ∧ b ≠ 0

@[simp]

theorem ENat.add_eq_add_left_iff {a b c : ℕ∞} : a + b = a + c ↔ b = c ∨ a = ⊤

@[simp]

theorem ENat.add_eq_add_right_iff {a b c : ℕ∞} : a + c = b + c ↔ a = b ∨ c = ⊤

@[simp]

theorem ENat.add_le_add_left_iff {a b c : ℕ∞} : a + b ≤ a + c ↔ b ≤ c ∨ a = ⊤

@[simp]

theorem ENat.add_le_add_right_iff {a b c : ℕ∞} : a + c ≤ b + c ↔ a ≤ b ∨ c = ⊤

@[simp]

theorem ENat.add_lt_add_left_iff {a b c : ℕ∞} : a + b < a + c ↔ b < c ∧ a ≠ ⊤

@[simp]

theorem ENat.add_lt_add_right_iff {a b c : ℕ∞} : a + c < b + c ↔ a < b ∧ c ≠ ⊤

@[simp]

theorem ENat.lt_add_one_self_iff {a : ℕ∞} : a < a + 1 ↔ a ≠ ⊤

@[simp]

theorem ENat.lt_one_add_self_iff {a : ℕ∞} : a < 1 + a ↔ a ≠ ⊤

theorem ENat.add_one_eq_add_one_iff {a b : ℕ∞} : a + 1 = b + 1 ↔ a = b

theorem ENat.one_add_eq_one_add_iff {a b : ℕ∞} : a + 1 = b + 1 ↔ a = b

theorem ENat.add_sub_cancel_right {b : ℕ∞} (a : ℕ∞) (hb : b ≠ ⊤) : a + b - b = a

theorem ENat.add_sub_cancel_left {a : ℕ∞} (b : ℕ∞) (ha : a ≠ ⊤) : a + b - a = b

theorem ENat.sub_eq_iff_eq_add {b a k : ℕ∞} (hka : k ≤ a) (hne : k ≠ ⊤) : a - k = b ↔ a = b + k

theorem ENat.mul_lt_mul_right_iff {a b c : ℕ∞} (hc0 : c ≠ 0) (hc : c ≠ ⊤) : a * c < b * c ↔ a < b

theorem ENat.mul_lt_mul_left_iff {a b c : ℕ∞} (hc0 : c ≠ 0) (hc : c ≠ ⊤) : c * a < c * b ↔ a < b

@[simp]

theorem ENat.even_top : Even ⊤

@[simp]

theorem ENat.odd_top : Odd ⊤

@[simp]

theorem ENat.even_natCast {n : ℕ} : Even ↑n ↔ Even n

@[simp]

theorem ENat.odd_natCast {n : ℕ} : Odd ↑n ↔ Odd n

theorem ENat.not_odd_iff_even {n : ℕ∞} (hn : n ≠ ⊤) : ¬Odd n ↔ Even n

theorem ENat.not_even_iff_odd {n : ℕ∞} (hn : n ≠ ⊤) : ¬Even n ↔ Odd n

theorem ENat.even_or_odd {a : ℕ∞} (ha : a ≠ ⊤) : Even a ∨ Odd a

theorem ENat.even_add {m n : ℕ∞} (hm : m ≠ ⊤) (hn : n ≠ ⊤) : Even (m + n) ↔ (Even m ↔ Even n)

theorem ENat.sInf_mem {s : Set ℕ∞} (h : s.Nonempty) : sInf s ∈ s

theorem ENat.exists_eq_iInf₂ {ι : Sort u_1} {κ : ι → Sort u_2} (f : (i : ι) → κ i → ℕ∞) (a₀ : ι) (b₀ : κ a₀) : ∃ (a : ι) (b : κ a), f a b = ⨅ (i : ι), ⨅ (j : κ i), f i j

theorem ENat.exists_eq_biInf {ι : Type u_1} {s : Set ι} (f : ι → ℕ∞) (hs : s.Nonempty) : ∃ a ∈ s, f a = ⨅ i ∈ s, f i

theorem ENat.exists_eq_biSup_of_lt_top {ι : Type u_1} {s : Set ι} (hs : s.Nonempty) (f : ι → ℕ∞) (hf : ⨆ i ∈ s, f i < ⊤) : ∃ a ∈ s, f a = ⨆ i ∈ s, f i