refl — Mathlib

English

If r and s are reflexive relations on α and β, then LiftRel r s is reflexive on α ⊕ₗ β, i.e. LiftRel r s x x for all x.

Русский

Если r и s — рефлексивные отношения на α и β, то LiftRel r s на α ⊕ₗ β тоже рефлексивно: для любого x выполняется LiftRel r s x x.

LaTeX

$$$\\text{refl} \\; (\\,r\\,)(x) \\land \\text{refl} \\; (\\,s\\,)(x) \\Rightarrow \\text{LiftRel } r s\\; x\\; x$$$

Lean4

@[refl]
theorem refl [IsRefl α r] [IsRefl β s] : ∀ x, LiftRel r s x x
  | inl a => LiftRel.inl (_root_.refl a)
  | inr a => LiftRel.inr (_root_.refl a)

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