map_inl_subset_iff_subset_toLeft

Mathlib.Data.Finset.Sum

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

English

Equivalence form: u = s ⊎ t if and only if u^{toLeft} = s and u^{toRight} = t.

Русский

Эквивалентная форма: u = s ⊎ t, если и только если u^{toLeft} = s и u^{toRight} = t.

LaTeX

$$u = s \uplus t \iff u^{\mathrm{toLeft}} = s \land u^{\mathrm{toRight}} = t$$

Lean4

theorem map_inl_subset_iff_subset_toLeft : s.map .inl ⊆ u ↔ s ⊆ u.toLeft := by simp [← disjSum_empty, disjSum_subset]

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

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

Разделы

Аффилиация

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