denselyOrdered — Mathlib

English

If s is a subsingleton subset of a type with LT, then the induced order on s is densely ordered (vacuous truth).

Русский

Если s — подсинглотонное подмножество типа с линейным порядком, то введённый на s порядок плотно упорядочен (вакуумная истина).

LaTeX

$$$ {s : Set \alpha} [LT \alpha] (hs : s.Subsingleton) : DenselyOrdered s $$$

Lean4

theorem denselyOrdered {s : Set α} [LT α] (hs : s.Subsingleton) : DenselyOrdered s :=
  have := (subsingleton_coe _).mpr hs
  ⟨fun _ _ h ↦ ⟨_, h.trans_eq (Subsingleton.elim _ _), h⟩⟩

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