cantorFunctionAux_zero

Mathlib.Analysis.Real.Cardinality

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

English

cantorFunctionAux c f 0 equals if f(0) then 1 else 0.

Русский

CantorFunctionAux c f 0 равно если f(0) то 1 иначе 0.

LaTeX

$$$ cantorFunctionAux\\ c\\ f\\ 0 = \\operatorname{cond}(f(0),1,0)$$$

Lean4

theorem cantorFunctionAux_zero (f : ℕ → Bool) : cantorFunctionAux c f 0 = cond (f 0) 1 0 := by
  cases h : f 0 <;> simp [h]

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

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

Разделы

Аффилиация

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