cantorFunctionAux_nonneg

Mathlib.Analysis.Real.Cardinality

URI: https://scilib.ai/kg/mathlib#Cardinal.cantorFunctionAux_nonneg

English

For any c, f, n, if f(n) = true then cantorFunctionAux c f n = c^n.

Русский

Для любых c, f, n, если f(n) = true, то cantorFunctionAux c f n = c^n.

LaTeX

$$$\\forall c f n, f(n) = \\text{true} \\Rightarrow \\operatorname{cantorFunctionAux} c f n = c^{n}$$$

Lean4

theorem cantorFunctionAux_nonneg (h : 0 ≤ c) : 0 ≤ cantorFunctionAux c f n :=
  by
  cases h' : f n
  · simp [h']
  · simpa [h'] using pow_nonneg h _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru