preimage_inr_image_inl

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.preimage_inr_image_inl

English

For any set s in α, the preimage of the inl-image of s under Sum.inr is empty.

Русский

Для любого множества s ⊆ α, предобраз образа inl через inr пуст.

LaTeX

$$$(\mathrm{Sum.inr})^{-1}(\mathrm{Sum.inl}'' s) = \emptyset$$$

Lean4

@[simp]
theorem preimage_inr_image_inl (s : Set α) : Sum.inr ⁻¹' (@Sum.inl α β '' s) = ∅ :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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