toLeft_eq_univ

Mathlib.Data.Fintype.Sum

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

English

For a Finset u of α ⊕ β, u.toLeft equals the universal Finset if and only if univ.map inl is a subset of u.

Русский

Для подмножества u над α ⊕ β, равенство u.toLeft = univ эквивалентно тому, что univ.map inl ⊆ u.

LaTeX

$$$u.toLeft = univ \;\iff\; univ.map .inl \subseteq u$$$

Lean4

theorem toLeft_eq_univ : u.toLeft = univ ↔ univ.map .inl ⊆ u := by simp [map_inl_subset_iff_subset_toLeft]

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

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

Разделы

Аффилиация

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