mk_wcovBy_mk_iff_right — Mathlib

English

Between copies with the same first component, WCovBy reduces to a WCovBy on the second components.

Русский

Между парами с одинаковым первым компонентом слабое покрытие сводится к слабому покрытию по вторым компонентам.

LaTeX

$$$ WCovBy{ fst := a, snd := b1 } { fst := a, snd := b2 } \iff WCovBy b1 b2 $$$

Lean4

theorem mk_wcovBy_mk_iff_right : (a, b₁) ⩿ (a, b₂) ↔ b₁ ⩿ b₂ :=
  swap_wcovBy_swap.trans mk_wcovBy_mk_iff_left

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