preimage_subtype_val_Iic — Mathlib

English

For any a in the subtype {x | p x}, the preimage of the ray (−∞, a.1] under the projection equals the ray (−∞, a] inside the subtype.

Русский

Для любого a из подтипа {x | p x} предобраз луча (−∞, a.1] под проекцией равен лучу (−∞, a] внутри подтипа.

LaTeX

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

Lean4

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

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