compression_idem — Mathlib

English

Compression is idempotent: applying 𝓓 a twice yields the same result as applying it once.

Русский

Компрессия идемпотентна: применение 𝓓 a дважды дает тот же результат, что и один раз.

LaTeX

$$$𝓓 a (𝓓 a 𝒜) = 𝓓 a 𝒜$$$

Lean4

/-- Down-compressing a family is idempotent. -/
@[simp]
theorem compression_idem (a : α) (𝒜 : Finset (Finset α)) : 𝓓 a (𝓓 a 𝒜) = 𝓓 a 𝒜 :=
  by
  ext s
  refine mem_compression.trans ⟨?_, fun h => Or.inl ⟨h, erase_mem_compression_of_mem_compression h⟩⟩
  rintro (h | h)
  · exact h.1
  · cases h.1 (mem_compression_of_insert_mem_compression h.2)

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