upShadow_compls — Mathlib

English

For any 𝒜, shadow of complement equals complement of shadow: ∂⁺ 𝒜ᶜˢ = (∂ 𝒜)ᶜˢ.

Русский

Для любого 𝒜 тень дополнения равна дополнению тени: ∂⁺ 𝒜ᶜˢ = (∂ 𝒜)ᶜˢ.

LaTeX

$$$ ∂⁺ 𝒜^{c\,s} = (∂ 𝒜)^{c\,s} $$$

Lean4

@[simp]
theorem upShadow_compls : ∂⁺ 𝒜ᶜˢ = (∂ 𝒜)ᶜˢ := by
  ext s
  simp only [mem_shadow_iff, mem_upShadow_iff, mem_compls]
  refine (compl_involutive.toPerm _).exists_congr_left.trans ?_
  simp [← compl_involutive.eq_iff]

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