part_subset

Mathlib.Order.Partition.Finpartition

URI: https://scilib.ai/kg/mathlib#Finpartition.part_subset

English

The part P.part a is a subset of s.

Русский

Часть P.part a является подмножеством s.

LaTeX

$$$ P.part a \subseteq s $$$

Lean4

@[simp]
theorem part_subset (a : α) : P.part a ⊆ s := by
  by_cases ha : a ∈ s
  · exact P.le <| P.part_mem.2 ha
  · simp [P.part_eq_empty.2 ha]

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

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

Разделы

Аффилиация

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