preimage_subtype_val_Icc — Mathlib

English

For any a,b in the subtype {x | p x}, the preimage of the closed interval [a.1, b] under the projection equals the closed interval [a, b] inside the subtype.

Русский

Для любых a,b из подтипа {x | p x} предобраз замкнутого отрезка [a.1, b] под проекцией равен [a, b] внутри подтипа.

LaTeX

$$$ \operatorname{val}^{-1}(\mathrm{Icc} a.1 b) = \mathrm{Icc} a b$$$

Lean4

@[simp]
theorem preimage_subtype_val_Icc (a b : { x // p x }) : (↑) ⁻¹' (Icc a.1 b) = Icc a b :=
  rfl

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