exists_mem

Mathlib.Order.Partition.Finpartition

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

English

For every a ∈ s there exists a part t ∈ P.parts with a ∈ t.

Русский

Для каждого a ∈ s существует часть t ∈ P.parts с a ∈ t.

LaTeX

$$$ a \in s \Rightarrow \exists t \in P.parts, a \in t $$$

Lean4

theorem exists_mem (ha : a ∈ s) : ∃ t ∈ P.parts, a ∈ t :=
  by
  simp_rw [← P.sup_parts] at ha
  exact mem_sup.1 ha

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

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

Разделы

Аффилиация

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