covBy_iff — Mathlib

English

For a dependent function a,b on an index set, if a ⩿ b then for every index i, a(i) ⩿ b(i).

Русский

Для функции с индексами, если a ⩿ b, то для каждого индекса i выполняется a(i) ⩿ b(i).

LaTeX

$$$ h : a \covby b \Rightarrow \forall i,\; a(i) \covby b(i) $$$

Lean4

theorem covBy_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_covBy_mk_iff

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