mk_wcovBy_mk_iff_left — Mathlib

English

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

Русский

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

LaTeX

$$$ WCovBy{ fst := a1, snd := b } { fst := a2, snd := b } \iff WCovBy a1 a2 $$$

Lean4

theorem mk_wcovBy_mk_iff_left : (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂ :=
  by
  refine ⟨WCovBy.fst, (And.imp mk_le_mk_iff_left.2) fun h c h₁ h₂ => ?_⟩
  have : c.2 = b := h₂.le.2.antisymm h₁.le.2
  rw [← @Prod.mk.eta _ _ c, this, mk_lt_mk_iff_left] at h₁ h₂
  exact h h₁ h₂

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