isCompressed_self — Mathlib

English

Every pair (u, u) makes the compression a valid compression; i.e., IsCompressed u u s always holds and thus compression is well-defined in this case.

Русский

Любая пара элементов (u, u) образует допустимое сжатие; IsCompressed u u s всегда выполняется.

LaTeX

$$IsCompressed(u,u,s)$$

Lean4

/-- Any family is compressed along two identical elements. -/
theorem isCompressed_self (u : α) (s : Finset α) : IsCompressed u u s :=
  compression_self u s

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