instIsRefl

Mathlib.Order.RelClasses

URI: https://scilib.ai/kg/mathlib#Order.Preimage.instIsRefl

English

If r is reflexive on α, then the preimage order on β, f⁻¹'∘ r, is reflexive.

Русский

Если $r$ рефлексивно на $\alpha$, то предобразный порядок на $\beta$, $f^{-1} o r$, рефлексивен.

LaTeX

$$IsRefl(β, (f⁻¹'o r))$$

Lean4

instance instIsRefl [IsRefl α r] {f : β → α} : IsRefl β (f ⁻¹'o r) :=
  ⟨fun _ => refl_of r _⟩

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

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

Разделы

Аффилиация

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