familyOfBFamily'

Mathlib.SetTheory.Ordinal.Family

URI: https://scilib.ai/kg/mathlib#Ordinal.familyOfBFamily'

← MathLib Explorer

English

If o < b, then log b o = 0.

Русский

Если o < b, то log_b o = 0.

LaTeX

$$$ o < b \Rightarrow \log_b o = 0 $$$

Lean4

/-- Converts a family indexed by an `Ordinal.{u}` to one indexed by a `Type u` using a specified
well-ordering. -/
def familyOfBFamily' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o} (ho : type r = o) (f : ∀ a < o, α) : ι → α :=
  fun i =>
  f (typein r i)
    (by
      rw [← ho]
      exact typein_lt_type r i)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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