exists_forall_eq_of_wcovBy — Mathlib

English

If a is weakly covered by b in the product, then there exists an index i such that all other coordinates agree, i.e., a_j = b_j for all j ≠ i.

Русский

Если a слабо покрывается b в произведении, то существует индекс i, при котором все остальные координаты совпадают: a_j = b_j для всех j ≠ i.

LaTeX

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

Lean4

theorem exists_forall_eq_of_wcovBy [Nonempty ι] (h : a ⩿ b) : ∃ i, ∀ j ≠ i, a j = b j :=
  by
  obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h
  exact ⟨i, fun j hj ↦ AntisymmRel.eq (hi _ hj)⟩

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