mem_copy_iff

Mathlib.Order.Partition.Basic

URI: https://scilib.ai/kg/mathlib#Partition.mem_copy_iff

Lean4

@[simp]
theorem mem_copy_iff {t x : α} {P : Partition s} (hst : s = t) : x ∈ P.copy hst ↔ x ∈ P :=
  Iff.rfl

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

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

Разделы

Аффилиация

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