imp_right — Mathlib

English

If C implies D, then LiftRelO R C implies LiftRelO R D (holding R fixed).

Русский

Если C ⇒ D, тогда LiftRelO R C ⇒ LiftRelO R D (при фиксированном R).

LaTeX

$$$$ (\forall o p,\ LiftRelO\ R\ C\ o p \to \LiftRelO\ R\ D\ o p) \quad \text{whence} \quad \text{LiftRelO}(R,C) \Rightarrow \text{LiftRelO}(R,D). $$$$

Lean4

theorem imp_right (R : α → β → Prop) {C D : WSeq α → WSeq β → Prop} (H : ∀ s t, C s t → D s t) {o p} :
    LiftRelO R C o p → LiftRelO R D o p :=
  LiftRelO.imp (fun _ _ => id) H

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