part_surjOn

Mathlib.Order.Partition.Finpartition

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

← MathLib Explorer

English

P.part is surjective from s onto P.parts.

Русский

P.part отображение из s на P.parts сюръективно.

LaTeX

$$$ Set.SurjOn(P.part, s, P.parts) $$$

Lean4

theorem part_surjOn : Set.SurjOn P.part s P.parts := fun p hp ↦
  by
  obtain ⟨x, hx⟩ := P.nonempty_of_mem_parts hp
  have hx' := mem_of_subset (P.le hp) hx
  use x, hx', (P.existsUnique_mem hx').unique ⟨P.part_mem.2 hx', P.mem_part hx'⟩ ⟨hp, hx⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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