rel_rfl

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

URI: https://scilib.ai/kg/mathlib#ValuativeRel.rel_rfl

English

Same as reflexivity: a basic reflexive property of the valuative relation.

Русский

То же самое, что и рефлексивность: базовое свойство рефлексивности отношения.

LaTeX

$$$ x \le\!_v x $$$

Lean4

theorem rel_rfl {x : R} : x ≤ᵥ x :=
  rel_refl x

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

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

Разделы

Аффилиация

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