preimage_inl

Mathlib.Data.Finset.Preimage

URI: https://scilib.ai/kg/mathlib#Finset.preimage_inl

English

Same as above; explicit form of the left injection case.

Русский

То же самое; явная форма для левой инъекции.

LaTeX

$$$$ \\text{same as previous: } s.preimage Sum.inl = s.toLeft. $$$$

Lean4

@[simp]
theorem preimage_inl (s : Finset (α ⊕ β)) : s.preimage Sum.inl Sum.inl_injective.injOn = s.toLeft := by ext x; simp

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

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

Разделы

Аффилиация

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