sectionsMk — Mathlib

English

When J is well-ordered, the sections Mk are defined by taking defaults from the extension and are compatible.

Русский

Если J хорошо упорядочен, секции Mk задаются через значения по умолчанию и согласованы.

LaTeX

$$$\\text{sectionsMk}:\\text{WellOrderInductionData} \\to \\text{sections}$$$

Lean4

/-- When `J` is a well-ordered type, `F : Jᵒᵖ ⥤ Type v`, and `d : F.WellOrderInductionData`,
this is the section of `F` that is determined by `val₀ : F.obj (op ⊥)` -/
noncomputable def sectionsMk (val₀ : F.obj (op ⊥)) : F.sections
    where
  val j := (default : d.Extension val₀ j.unop).val
  property := fun f ↦ by apply Extension.compatibility

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