subtype_Ioc_eq — Mathlib

English

For Ioc intervals, Ioc a b on the subtype equals the subtype of Ioc interval in α: Ioc a b = (Ioc(a.val, b.val)).subtype p.

Русский

Интервал Ioc на подтипе равен подтипу интервала Ioc в α: Ioc a b = (Ioc(a.val, b.val)).subtype p.

LaTeX

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

Lean4

theorem subtype_Ioc_eq : Ioc a b = (Ioc (a : α) b).subtype p :=
  rfl

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