powerlt_le — Mathlib

English

For cardinals a, b, c: a^{<b} ≤ c if and only if for every x < b, a^{x} ≤ c.

Русский

Для кардиналов a, b, c верно: a^{<b} ≤ c тогда и только тогда, когда для каждого x < b выполняется a^{x} ≤ c.

LaTeX

$$$a^{< b} \\le c \\\\Leftrightarrow \\\\forall x < b, a^x \\le c$$$

Lean4

theorem powerlt_le {a b c : Cardinal.{u}} : a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c :=
  by
  rw [powerlt, ciSup_le_iff']
  · simp
  · rw [← image_eq_range]
    exact bddAbove_image.{u, u} _ bddAbove_Iio

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