compress_sdiff_sdiff — Mathlib

English

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

Русский

Если s принадлежит 𝒜, то s.erase a принадлежит 𝓓 a 𝒜.

LaTeX

$$$s \\in 𝒜 \\Rightarrow s \\setminus \\{a\\} \\in 𝓓 a 𝒜$$$

Lean4

/-- An element can be compressed to any other element by removing/adding the differences. -/
@[simp]
theorem compress_sdiff_sdiff (a b : α) : compress (a \ b) (b \ a) b = a :=
  by
  refine (compress_of_disjoint_of_le disjoint_sdiff_self_left sdiff_le).trans ?_
  rw [sup_sdiff_self_right, sup_sdiff, disjoint_sdiff_self_right.sdiff_eq_left, sup_eq_right]
  exact sdiff_sdiff_le

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