preimage_inl_range_inr

Mathlib.Data.Set.Image

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

English

The preimage of the range of inr under inl is empty.

Русский

Предобраз образа inr под inl пуст.

LaTeX

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

Lean4

@[simp]
theorem preimage_inl_range_inr : Sum.inl ⁻¹' range (Sum.inr : β → α ⊕ β) = ∅ := by
  rw [← image_univ, preimage_inl_image_inr]

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

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

Разделы

Аффилиация

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