preimage_subtype_val_Ici — Mathlib

English

For any a in the subtype {x | p x}, the preimage of the ray [a.1, ∞) under the projection to α equals the ray [a, ∞) inside the subtype.

Русский

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

LaTeX

$$$ \operatorname{val}^{-1}(\mathrm{Icc?}) = \mathrm{Ici} a$$$

Lean4

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

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