subtype_Iic_eq_Icc — Mathlib

English

For x ∈ the unit interval, the set of y in I such that y ≤ x is exactly the closed interval [0, x].

Русский

Для x ∈ единичного интервала множество y ∈ I, удовлетворяющих y ≤ x, равно замкнутому интервалу [0, x].

LaTeX

$$preimage(Subtype.val) (Iic x) = Icc 0 x, for x ∈ I$$

Lean4

theorem subtype_Iic_eq_Icc (x : I) : Subtype.val ⁻¹' (Iic ↑x) = Icc 0 x :=
  by
  rw [preimage_subtype_val_Iic]
  exact Icc_bot.symm

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