preimage_coe_Iio_top — Mathlib

English

Let i: α → WithTop α be the embedding. Then the preimage of Iio ⊤ equals the whole space, i.e., univ.

Русский

Пусть i: α → WithTop α — вложение. Тогда прообраз Iio ⊤ равен всю область, то есть univ.

LaTeX

$$$$(\text{WithTop.some})^{-1} \bigl( \mathrm{Iio}(\top) \bigr) = \mathrm{univ}$$$$

Lean4

@[simp]
theorem preimage_coe_Iio_top : (some : α → WithTop α) ⁻¹' Iio ⊤ = univ := by rw [← range_coe, preimage_range]

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