transfiniteIterate_bot — Mathlib

English

The base case of transfinite iteration: transfiniteIterate φ (⊥ : J) i₀ = i₀.

Русский

Базовый случай трансфинитной итерации: transfiniteIterate φ (⊥ : J) i₀ = i₀.

LaTeX

$$$transfiniteIterate\\,φ\\,(\\perp\\;:J)\\,i_0 = i_0$$$

Lean4

@[simp]
theorem transfiniteIterate_bot [OrderBot J] (i₀ : I) : transfiniteIterate φ (⊥ : J) i₀ = i₀ :=
  by
  dsimp [transfiniteIterate]
  simp only [isMin_iff_eq_bot, SuccOrder.limitRecOn_isMin, id_eq]

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