instInhabitedInductiveLimitOfOfNatNat

Mathlib.Topology.MetricSpace.Gluing

URI: https://scilib.ai/kg/mathlib#Metric.instInhabitedInductiveLimitOfOfNatNat

Lean4

instance (I : ∀ n, Isometry (f n)) [Inhabited (X 0)] : Inhabited (InductiveLimit I) :=
  ⟨toInductiveLimit _ 0 default⟩

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

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

Разделы

Аффилиация

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