mem_shadow_iff_exists_sdiff — Mathlib

English

t ∈ ∂ 𝒜 iff there exists s ∈ 𝒜 such that t ⊆ s and erase s a = t for some a ∈ s.

Русский

t ∈ ∂ 𝒜 тогда и только тогда, когда существует s ∈ 𝒜 такое, что t ⊆ s и для некоторого a ∈ s выполняется erase s a = t.

LaTeX

$$$$ t \\in ∂ 𝒜 \\iff \\exists s \\in 𝒜, \\exists a \\in s, \\mathrm{erase}(s,a) = t $$$$

Lean4

/-- `t ∈ ∂𝒜` iff `t` is exactly one element less than something from `𝒜`.

See also `Finset.mem_shadow_iff_exists_mem_card_add_one`. -/
theorem mem_shadow_iff_exists_sdiff : t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = 1 := by
  simp_rw [mem_shadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase]

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