instIsReflSubtype

Mathlib.Order.RelIso.Set

URI: https://scilib.ai/kg/mathlib#Subrel.instIsReflSubtype

English

If r is reflexive on α, then the induced relation on the subtype p is reflexive.

Русский

Если r на α рефлексивно, то ограничение Subrel r p на подпредикате p также рефлексивно.

LaTeX

$$$ \\forall a:\\alpha,\\ p(a)\\rightarrow r(a,a). $$$

Lean4

instance (r : α → α → Prop) [IsRefl α r] (p : α → Prop) : IsRefl _ (Subrel r p) :=
  ⟨fun x => @IsRefl.refl α r _ x⟩

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

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

Разделы

Аффилиация

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