IccInclusionLeft — Mathlib

English

There is a natural continuous map embedding the left subinterval Icc a b into Icc a c; this is an order-preserving embedding.

Русский

Существуют естественное непрерывное вложение левого подотрезка Icc a b в Icc a c; это отображение сохраняет порядок.

LaTeX

$$$\\text{IccInclusionLeft} : C(Icc a b, Icc a c)$ с естественной вложенностью левых концов.$$

Lean4

/-- The embedding into an interval from a sub-interval lying on the left, as a `ContinuousMap`. -/
def IccInclusionLeft : C(Icc a b, Icc a c) :=
  .inclusion <| Icc_subset_Icc le_rfl Fact.out

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