of_eq

Mathlib.Order.Defs.Unbundled

URI: https://scilib.ai/kg/mathlib#of_eq

English

If r is reflexive on α, then equality implies r(a,b) for all a,b.

Русский

Если отношение r на α рефлексивно, то равенство a = b подразумевает r(a,b).

LaTeX

$$$\\\\forall a,b, \\\\ a = b \\\\Rightarrow r(a,b).$$$

Lean4

theorem of_eq [IsRefl α r] : ∀ {a b}, a = b → r a b
  | _, _, .refl _ => refl _

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

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

Разделы

Аффилиация

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