preimage_coe_Icc — Mathlib

English

The embedding φ preserves closed intervals: for all a,b ∈ α, φ^{-1}(Icc(a,b)) = Icc(a,b).

Русский

Встраивание φ сохраняет замкнутые интервалы: для всех a,b ∈ α выполняется φ^{-1}(Icc(a,b)) = Icc(a,b).

LaTeX

$$$ \forall a,b \in \alpha, \ \phi^{-1}(\mathrm{Icc}(a,b)) = \mathrm{Icc}(a,b). $$$

Lean4

@[simp]
theorem preimage_coe_Icc : (some : α → WithBot α) ⁻¹' Icc a b = Icc a b := by simp [← Ici_inter_Iic]

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