preimage_coe_Ioo — Mathlib

English

Let i: α → WithTop α be the embedding. Then the preimage of Ioo(i(a), i(b)) under i equals Ioo(a, b).

Русский

Пусть i: α → WithTop α — вложение. Тогда прообраз Ioo(i(a), i(b)) через i равен Ioo(a, b).

LaTeX

$$$$(\text{WithTop.some})^{-1}\bigl(\mathrm{Ioo}(\text{WithTop.some } a, \text{WithTop.some } b)\bigr) = \mathrm{Ioo}(a,b)$$$$

Lean4

@[simp]
theorem preimage_coe_Ioo : (some : α → WithTop α) ⁻¹' Ioo a b = Ioo a b := by simp [← Ioi_inter_Iio]

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