English
CovBy between pairs is equivalent to a mixed condition on coordinates: either the first coordinates are in covBy and seconds equal, or seconds are in covBy and first coordinates equal.
Русский
CovBy между парами эквивалентен смешанному условию по координатам: либо первые координаты в CovBy и вторые равны, либо вторые в CovBy и первые равны.
LaTeX
$$$ CovBy { fst := a1, snd := b1 } { fst := a2, snd := b2 } \iff ( a1 \ covBy a2 \wedge b1 = b2 ) \lor ( b1 \ covBy b2 \wedge a1 = a2 ) $$$
Lean4
theorem mk_covBy_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.wcovBy
· exact Or.inr ⟨mk_covBy_mk_iff_right.1 h, rfl⟩
· exact Or.inl ⟨mk_covBy_mk_iff_left.1 h, rfl⟩
· rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)
· exact mk_covBy_mk_iff_left.2 h
· exact mk_covBy_mk_iff_right.2 h
