proj_eq_iff

Mathlib.Data.Setoid.Partition

URI: https://scilib.ai/kg/mathlib#IndexedPartition.proj_eq_iff

English

For any x,y ∈ α, hs.proj x = hs.proj y if and only if hs.index x = hs.index y.

Русский

Для любых x,y ∈ α верно: hs.proj x = hs.proj y тогда и только если hs.index x = hs.index y.

LaTeX

$$$ hs.proj x = hs.proj y \iff hs.index x = hs.index y $$$

Lean4

theorem proj_eq_iff {x y : α} : hs.proj x = hs.proj y ↔ hs.index x = hs.index y :=
  Quotient.eq''

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

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

Разделы

Аффилиация

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