le_powerlt — Mathlib

English

Let a, b, c be cardinals with c < b. Then a^c ≤ a^<b, where a^<b denotes the supremum of a^x for x < b.

Русский

Пусть a, b, c — кардиналы и c < b. Тогда a^c ≤ a^{<b}, где a^{<b} обозначает верхнюю границу множества {a^x : x < b}.

LaTeX

$$$a^c \\le a^{< b}$$$

Lean4

theorem le_powerlt {b c : Cardinal.{u}} (a) (h : c < b) : (a ^ c) ≤ a ^< b :=
  by
  refine le_ciSup (f := fun y : Iio b => a ^ (y : Cardinal)) ?_ ⟨c, h⟩
  rw [← image_eq_range]
  exact bddAbove_image.{u, u} _ bddAbove_Iio

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