liftRel_think_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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