mem_upShadow_iff_exists_sdiff — Mathlib

English

t is in the upper shadow ∂⁺ 𝒜 iff ∃ s ∈ 𝒜, s ⊆ t and #(t \ s) = 1.

Русский

t принадлежит верхней тени ∂⁺ 𝒜 тогда, когда существует s ∈ 𝒜 с s ⊆ t и #(t \ s) = 1.

LaTeX

$$$ t ∈ ∂⁺ 𝒜 \iff ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = 1 $$$

Lean4

/-- `t` is in the upper shadow of `𝒜` iff `t` is exactly one element more than something from `𝒜`.

See also `Finset.mem_upShadow_iff_exists_mem_card_add_one`. -/
theorem mem_upShadow_iff_exists_sdiff : t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = 1 := by
  simp_rw [mem_upShadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]

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