liftRel_think_left — Mathlib

English

Replacing the left argument by think does not change LiftRel: LiftRel R (think s) t iff LiftRel R s t.

Русский

Замена левого аргумента think на s не изменяет LiftRel: LiftRel R (think s) t ⇔ LiftRel R s t.

LaTeX

$$$\mathrm{LiftRel}\ R\ (\mathrm{think}\ s)\ t \iff \mathrm{LiftRel}\ R\ s\ t$$$

Lean4

@[simp]
theorem liftRel_think_left (R : α → β → Prop) (s t) : LiftRel R (think s) t ↔ LiftRel R s t := by
  rw [liftRel_destruct_iff, liftRel_destruct_iff]; simp

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