refl — Mathlib

English

The lifted relation is reflexive when the base relation is reflexive.

Русский

Поднятое отношение рефлексивно при условии рефлексивности базового отношения.

LaTeX

$$$$ \forall {\alpha},\ \mathrm{Refl}(R) \Rightarrow \mathrm{Reflexive}(\mathrm{LiftRel}\ R). $$$$

Lean4

theorem refl (R : α → α → Prop) (H : Reflexive R) : Reflexive (LiftRel R) := fun s =>
  by
  refine ⟨(· = ·), rfl, fun {s t} (h : s = t) => ?_⟩
  rw [← h]
  apply Computation.LiftRel.refl
  intro a
  rcases a with - | a
  · simp
  · cases a
    simp only [LiftRelO, and_true]
    apply H

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