subtype_Ico_eq — Mathlib

English

Under LocallyFiniteOrder, the Ico interval on the subtype matches the subtype of the Ico interval in α: Ico a b = (Ico(a.val, b.val)).subtype p.

Русский

При LocallyFiniteOrder интервал Ico на подтипе совпадает с подтипом интервала Ico в α: Ico a b = (Ico(a.val, b.val)).subtype p.

LaTeX

$$$$ \\mathrm{Ico}(a,b) = \\mathrm{subtype}\\ p\\bigl( \\mathrm{Ico}(a.\\mathrm{val}, b.\\mathrm{val}) \\bigr). $$$$

Lean4

theorem subtype_Ico_eq : Ico a b = (Ico (a : α) b).subtype p :=
  rfl

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