wcovBy_iff — Mathlib

English

A pair is in the weak cover relation if and only if either the first coordinates are in WCovBy and second coordinates are equal, or the second coordinates are in WCovBy and first coordinates are equal.

Русский

Пара находится в слабом покрытии тогда и только тогда, когда либо первые координаты удовлетворяют WCovBy и вторые равны, либо вторые WCovBy и первые равны.

LaTeX

$$$ x \covBy y \iff x.1 \covBy y.1 \wedge x.2 = y.2 \lor x.2 \covBy y.2 \wedge x.1 = y.1 $$$

Lean4

theorem wcovBy_iff : x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1 :=
  by
  cases x
  cases y
  exact mk_wcovBy_mk_iff

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