subsingleton_next — Mathlib

English

For every i, the set { j | c.Rel i j } is a subsingleton; there is at most one j related to i.

Русский

Для каждого i множество { j | c.Rel i j } является единичным подмножеством; связано не более с одним j.

LaTeX

$$For all i, Subsingleton\{ j \mid c.Rel i j \}$$

Lean4

instance subsingleton_next (c : ComplexShape ι) (i : ι) : Subsingleton { j // c.Rel i j } :=
  by
  constructor
  rintro ⟨j, rij⟩ ⟨k, rik⟩
  congr
  exact c.next_eq rij rik

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