preimage_subtype_val_Ioo — Mathlib

English

For any a,b in the subtype {x | p x}, the preimage of the open interval (a.1, b) under the projection equals the open interval (a, b) inside the subtype.

Русский

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

LaTeX

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

Lean4

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

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