lt_cof_power — Mathlib

English

If a ≥ ℵ0 and 1 < b, then a < (b^a).ord.cof.

Русский

Если a ≥ ℵ0 и b > 1, то a < cof(ord(b^a)).

LaTeX

$$$$ \aleph_0 \le a \;\Rightarrow\; a < (b^a).ord.cof. $$$$

Lean4

theorem lt_cof_power {a b : Cardinal} (ha : ℵ₀ ≤ a) (b1 : 1 < b) : a < (b ^ a).ord.cof :=
  by
  have b0 : b ≠ 0 := (zero_lt_one.trans b1).ne'
  apply lt_imp_lt_of_le_imp_le (power_le_power_left <| power_ne_zero a b0)
  rw [← power_mul, mul_eq_self ha]
  exact lt_power_cof (ha.trans <| (cantor' _ b1).le)

Похожие утверждения