compress_idem — Mathlib

English

If s ∈ 𝓓 a 𝒜, then s.erase a ∈ 𝓓 a 𝒜.

Русский

Если s ∈ 𝓓 a 𝒜, то s.erase a ∈ 𝓓 a 𝒜.

LaTeX

$$$s \\in 𝓓(a,\\mathcal{A}) \\Rightarrow s\\setminus\\{a\\} \\in 𝓓(a,\\mathcal{A})$$$

Lean4

/-- Compressing an element is idempotent. -/
@[simp]
theorem compress_idem (u v a : α) : compress u v (compress u v a) = compress u v a :=
  by
  unfold compress
  split_ifs with h h'
  · rw [le_sdiff_right.1 h'.2, sdiff_bot, sdiff_bot, sup_assoc, sup_idem]
  · rfl
  · rfl

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