subsingleton_prev — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance subsingleton_prev (c : ComplexShape ι) (j : ι) : Subsingleton { i // c.Rel i j } :=
  by
  constructor
  rintro ⟨i, rik⟩ ⟨j, rjk⟩
  congr
  exact c.prev_eq rik rjk

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