isRefl

Mathlib.Order.RelIso.Basic

URI: https://scilib.ai/kg/mathlib#RelEmbedding.isRefl

English

If s is reflexive on β, then r is reflexive on α.

Русский

Если s рефлексивно на β, то r рефлексивно на α.

LaTeX

$$$\forall a.\ r(a,a).$$$

Lean4

protected theorem isRefl (f : r ↪r s) [IsRefl β s] : IsRefl α r :=
  ⟨fun _ => f.map_rel_iff.1 <| refl _⟩

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

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

Разделы

Аффилиация

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