English
Relation between WCovBy on a product and a combination of coordinate WCovBy relations plus equalities.
Русский
Связь между WCovBy на произведении и сочетанием координатных WCovBy вместе с равенствами координат.
LaTeX
$$$ WCovBy { fst := a1, snd := b1 } { fst := a2, snd := b2 } \iff ( WCovBy a1 a2 \wedge b1 = b2 ) \lor ( WCovBy b1 b2 \wedge a1 = a2 ) $$$
Lean4
theorem mk_wcovBy_mk_iff : (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂ :=
by
refine ⟨fun h => ?_, ?_⟩
· obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h
· exact Or.inr ⟨mk_wcovBy_mk_iff_right.1 h, rfl⟩
· exact Or.inl ⟨mk_wcovBy_mk_iff_left.1 h, rfl⟩
· rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)
· exact mk_wcovBy_mk_iff_left.2 h
· exact mk_wcovBy_mk_iff_right.2 h
