exists_forall_eq_of_covBy — Mathlib

English

If a is covered by b in the product, then there is a single coordinate i where a_i and b_i can differ, and all other coordinates must be equal.

Русский

Если a покрывается b в произведении, то существует одна координата i, в которой a_i и b_i могут различаться, а остальные координаты равны.

LaTeX

$$$a \\bowtie b \\Rightarrow \\exists i, \\forall j \\neq i, a_j = b_j$$$

Lean4

theorem exists_forall_eq_of_covBy (h : a ⋖ b) : ∃ i, ∀ j ≠ i, a j = b j :=
  by
  obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_covBy h
  exact ⟨i, fun j hj ↦ AntisymmRel.eq (hi _ hj)⟩

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