mk — Mathlib · SciLib

English

The constructor mk builds a Semiquot α from a witness a ∈ s, yielding a Semiquot with s and the truncated witness.

Русский

Конструктор mk образует Semiquot α из элемента a ∈ s, задавая Semiquot с множеством s и усечённым свидетельством.

LaTeX

$${a : α} {s : Set α} (h : a ∈ s) : Semiquot α$$

Lean4

/-- Construct a `Semiquot α` from `h : a ∈ s` where `s : Set α`. -/
def mk {a : α} {s : Set α} (h : a ∈ s) : Semiquot α :=
  ⟨s, Trunc.mk ⟨a, h⟩⟩

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