coeHom — Mathlib

English

A nonempty interval a can be viewed as the closed interval Icc(s.fst, s.snd) in α; the embedding is the natural identification of these two concepts.

Русский

Ненулевой интервал можно рассматривать как замкнутый интервал Icc(с.окончания) в α; естественным образом эти понятия совпадают через отображение.

LaTeX

$$$\mathrm{coeHom}(s) = \mathrm{Icc}(s.fst,s.snd)$$$

Lean4

/-- Consider a nonempty interval `[a, b]` as the set `[a, b]`. -/
def coeHom : NonemptyInterval α ↪o Set α :=
  OrderEmbedding.ofMapLEIff (fun s => Icc s.fst s.snd) fun s _ => Icc_subset_Icc_iff s.fst_le_snd

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