mk — Mathlib · SciLib

English

There is a constructor mk sending x ∈ A to an object of const n A α with B mapping to PEmpty.

Русский

Существует конструктор mk, который отправляет x ∈ A в объект константного функторa с данным значением и B-компонентой, равной пустоте.

LaTeX

$$$$ \\mathrm{const}.mk(n,A)(x) = \\langle x, \\lambda\\_ _ . PEmpty.elim \\rangle. $$$$

Lean4

/-- Constructor for the constant functor -/
def mk (x : A) {α} : const n A α :=
  ⟨x, fun _ a => PEmpty.elim a⟩

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