coe_one — Mathlib

English

Let α be a partially ordered set with a distinguished unit 1. The set represented by the element 1 in NonemptyInterval α is exactly the singleton {1}.

Русский

Пусть α упорядочено и задан единичный элемент 1. Множество, соответствующее элементу 1 в NonemptyInterval α, есть ровно множество {1}.

LaTeX

$$$((1 : \\mathrm{NonemptyInterval}\\ \\alpha) : \\mathrm{Set}\\ \\alpha) = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_one : ((1 : NonemptyInterval α) : Set α) = 1 :=
  coe_pure _

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