mono

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Relation.ReflGen.mono

Lean4

theorem mono {p : α → α → Prop} (hp : ∀ a b, r a b → p a b) : ∀ {a b}, ReflGen r a b → ReflGen p a b
  | a, _, ReflGen.refl => by rfl
  | a, b, single h => single (hp a b h)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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