isRefl_mono

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.isRefl_mono

English

If R1 is reflexive and R1 ⊆ R2, then R2 is reflexive.

Русский

Если R1 рефлексивно и R1 ⊆ R2, тогда R2 рефлексивно.

LaTeX

$$([R1.IsRefl]) \langle hR : R1 \subseteq R2 \rangle : R2.IsRefl$$

Lean4

theorem isRefl_mono [R₁.IsRefl] (hR : R₁ ⊆ R₂) : R₂.IsRefl where refl _ := hR R₁.rfl

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

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

Разделы

Аффилиация

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