toRight_eq_empty

Mathlib.Data.Fintype.Sum

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

English

For a Finset u of α ⊕ β, u.toRight is empty iff u ⊆ univ.map inl.

Русский

Для Finset u над α ⊕ β, u.toRight пусто тогда и только тогда, когда u ⊆ univ.map inl.

LaTeX

$$$u.toRight = ∅ \;\iff\; u \subseteq univ.map .inl$$$

Lean4

theorem toRight_eq_empty : u.toRight = ∅ ↔ u ⊆ univ.map .inl := by simp [subset_map_inl]

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

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

Разделы

Аффилиация

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