mem_upShadow_iff_exists_mem_card_add_one

English

t ∈ ∂⁺ 𝒜 iff ∃ s ∈ 𝒜, s ⊆ t ∧ #(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 less than something from `𝒜`.

See also `Finset.mem_upShadow_iff_exists_sdiff`. -/
theorem mem_upShadow_iff_exists_mem_card_add_one : t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + 1 :=
  by
  refine
    mem_upShadow_iff_exists_sdiff.trans <| exists_congr fun t ↦ and_congr_right fun _ ↦ and_congr_right fun hst ↦ ?_
  rw [card_sdiff_of_subset hst, tsub_eq_iff_eq_add_of_le, add_comm]
  exact card_mono hst

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