liftRel_mem_cases — Mathlib

English

If for every a in ca the LiftRel R ca cb holds and for every b in cb the LiftRel R ca cb holds, then LiftRel R ca cb holds.

Русский

Если для каждого a∈ca LiftRel R ca cb выполняется и для каждого b∈cb LiftRel R ca cb выполняется, тогда LiftRel R ca cb выполняется.

LaTeX

$$$\\big( \\forall a\\in ca,\\mathrm{LiftRel}\\,R\\ ca\\ cb \\big) \\\\to \\\\big( \\forall b\\in cb,\\mathrm{LiftRel}\\,R\\ ca\\ cb \\big) \\\\to \\\\mathrm{LiftRel}\\,R\\ ca\\ cb$$

Lean4

theorem liftRel_mem_cases {R : α → β → Prop} {ca cb} (Ha : ∀ a ∈ ca, LiftRel R ca cb) (Hb : ∀ b ∈ cb, LiftRel R ca cb) :
    LiftRel R ca cb :=
  ⟨fun {_} ma => (Ha _ ma).left ma, fun {_} mb => (Hb _ mb).right mb⟩

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