refl

Mathlib.Topology.DiscreteQuotient

URI: https://scilib.ai/kg/mathlib#DiscreteQuotient.refl

English

For every x in X, x is related to itself by the quotient relation.

Русский

Для каждого x ∈ X выполняется x эквивалентен самому себе по отношению эквивалентности, задаваемому факторизацией.

LaTeX

$$$ \\forall x \\in X,\\ x \\sim_S x $$$

Lean4

theorem refl : ∀ x, S.toSetoid x x :=
  S.refl'

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

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

Разделы

Аффилиация

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