map_inr_subset_iff_subset_toRight

Mathlib.Data.Finset.Sum

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

English

The left-inl subset equivalence: s.map inl ⊆ u ⇔ s ⊆ u^{toLeft}.

Русский

Эквивалентность включения: \mathrm{map}_{\mathrm{inl}}(s) ⊆ u ⇔ s ⊆ u^{toLeft}.

LaTeX

$$(\mathrm{map} \mathrm{inl}\, s) \subseteq u \iff s \subseteq u^{\mathrm{toLeft}}$$

Lean4

theorem map_inr_subset_iff_subset_toRight : t.map .inr ⊆ u ↔ t ⊆ u.toRight := by simp [← empty_disjSum, disjSum_subset]

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

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

Разделы

Аффилиация

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