preimage_coe_inter_self

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Subtype.preimage_coe_inter_self

English

The preimage of t ∩ s equals the preimage of t.

Русский

Предобраз включения от t ∩ s равен предобразу t.

LaTeX

$$$ (\uparrow)^{-1}(t \cap s) = (\uparrow)^{-1}(t) $$$

Lean4

theorem preimage_coe_inter_self (s t : Set α) : ((↑) : s → α) ⁻¹' (t ∩ s) = ((↑) : s → α) ⁻¹' t := by
  rw [inter_comm, preimage_coe_self_inter]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru