symm — Mathlib

English

LiftRel R is symmetric if R is symmetric.

Русский

LiftRel R симметрично, если R симметрично.

LaTeX

$$$\forall x y, \operatorname{LiftRel} R x y \Rightarrow \operatorname{LiftRel} R y x$$$

Lean4

theorem symm (R : α → α → Prop) (H : Symmetric R) : Symmetric (LiftRel R) := fun _ _ ⟨l, r⟩ =>
  ⟨fun {_} a2 =>
    let ⟨b, b1, ab⟩ := r a2
    ⟨b, b1, H ab⟩,
    fun {_} a1 =>
    let ⟨b, b2, ab⟩ := l a1
    ⟨b, b2, H ab⟩⟩

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