English
If a ≥ 0, the closed interval [0,a] in ℝ is order-isomorphic to the interval (−∞,a] in Set.
Русский
Если a ≥ 0, замыкаемое множество [0,a] в ℝ изоморфно по порядку интервалу (−∞,a] в множестве.
LaTeX
$$$ [0,a] \\cong_o (-\\infty, a] , \\quad a \\ge 0, $$$
Lean4
/-- If `a` is a nonnegative real number, then the closed interval `[0, a]` in `ℝ` is order
isomorphic to the interval `Set.Iic a`. -/
-- TODO: if we use `@[simps!]` it will look through the `NNReal = Subtype _` definition,
-- but if we use `@[simps]` it will not look through the `Equiv.Set.sep` definition.
-- Turning `NNReal` into a structure may be the best way to go here.
-- @[simps!? apply_coe_coe]
def orderIsoIccZeroCoe (a : ℝ≥0) : Set.Icc (0 : ℝ) a ≃o Set.Iic a
where
toEquiv := Equiv.Set.sep (Set.Ici 0) fun x : ℝ => x ≤ a
map_rel_iff' := Iff.rfl
