mem_upShadow_iff_erase_mem — Mathlib

English

t ∈ ∂⁺ 𝒜 iff ∃ a, a ∈ t and erase t a ∈ 𝒜.

Русский

t ∈ ∂⁺ 𝒜 тогда и только тогда, когда ∃ a, a ∈ t и erase t a ∈ 𝒜.

LaTeX

$$$ t ∈ ∂⁺ 𝒜 \iff ∃ a, a ∈ t ∧ erase t a ∈ 𝒜 $$$

Lean4

/-- `t` is in the upper shadow of `𝒜` iff we can remove an element from it so that the resulting
finset is in `𝒜`. -/
theorem mem_upShadow_iff_erase_mem : t ∈ ∂⁺ 𝒜 ↔ ∃ a, a ∈ t ∧ erase t a ∈ 𝒜 :=
  by
  simp_rw [mem_upShadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase]
  aesop

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