sumSet_preimage_inl

Mathlib.Logic.Embedding.Set

URI: https://scilib.ai/kg/mathlib#Function.Embedding.sumSet_preimage_inl

English

The preimage of r under inl via sumSet is r ∩ s.

Русский

Обратное изображение через inl по sumSet равно r ∩ s.

LaTeX

$$$.inl^{-1}(\\text{sumSet } h^{-1}(r)) = r \\cap s$$$

Lean4

@[simp]
theorem sumSet_preimage_inl (h : Disjoint s t) : .inl ⁻¹' (Function.Embedding.sumSet h ⁻¹' r) = r ∩ s := by
  simp [Set.ext_iff]

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

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

Разделы

Аффилиация

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