imp — Mathlib

English

If R a b implies S a b for all a,b, then LiftRel R s t implies LiftRel S s t.

Русский

Если R a b ⇒ S a b для всех a,b, то LiftRel R s t ⇒ LiftRel S s t.

LaTeX

$$$\\forall {R S: \\alpha \\to \\beta \\to \\mathrm{Prop}},\\ (\\forall {a b}, R\\ a\\ b \\rightarrow S\\ a\\ b) \\rightarrow \\forall s t,\\ \\mathrm{LiftRel}\\,R\\ s\\ t \\rightarrow \\mathrm{LiftRel}\\,S\\ s\\ t$$$

Lean4

theorem imp {R S : α → β → Prop} (H : ∀ {a b}, R a b → S a b) (s t) : LiftRel R s t → LiftRel S s t
  | ⟨l, r⟩ =>
    ⟨fun {_} as =>
      let ⟨b, bt, ab⟩ := l as
      ⟨b, bt, H ab⟩,
      fun {_} bt =>
      let ⟨a, as, ab⟩ := r bt
      ⟨a, as, H ab⟩⟩

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