mem_shadow_iff_exists_mem_card_add_one

English

t ∈ ∂ 𝒜 iff there exists a ∉ t such that insert a t ∈ 𝒜.

Русский

t ∈ ∂ 𝒜 тогда существует a, не принадлежащий t, такое что insert a t ∈ 𝒜.

LaTeX

$$$$ t \\in ∂ 𝒜 \\iff \\exists a \\notin t, \\ \\mathrm{insert}(a,t) \\in 𝒜 $$$$

Lean4

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

See also `Finset.mem_shadow_iff_exists_sdiff`. -/
theorem mem_shadow_iff_exists_mem_card_add_one : t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #s = #t + 1 :=
  by
  refine mem_shadow_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

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