toLeft_eq_empty

Mathlib.Data.Fintype.Sum

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

English

For a Finset u of α ⊕ β, u.toLeft equals ∅ iff u ⊆ univ.map inr.

Русский

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

LaTeX

$$$u.toLeft = ∅ \;\iff\; u \subseteq univ.map .inr$$$

Lean4

theorem toLeft_eq_empty : u.toLeft = ∅ ↔ u ⊆ univ.map .inr := by simp [subset_map_inr]

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

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

Разделы

Аффилиация

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