image_coe_preimage_symm — Mathlib

English

For any set s of unitInterval, the image of the coercion of the σ-preimage of s equals the σ-preimage of the image of s under the real-coercion.

Русский

Для любого множества s единичного интервала образ приведения предобраза σ множества s через приведенные к действительным числам равен предобразу σ через отображение к действительным числам от образа s.

LaTeX

$$$$ \operatorname{Set.image} \operatorname{Subtype.val} (\sigma^{-1}' s) = (1-\cdot)^{-1}' (\operatorname{Subtype.val}'' s). $$$$

Lean4

theorem image_coe_preimage_symm {s : Set I} : Subtype.val '' (σ ⁻¹' s) = (1 - ·) ⁻¹' (Subtype.val '' s) := by
  simp [symm_involutive, ← Function.Involutive.image_eq_preimage, image_image]

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