mem_shadow_iff_insert_mem — Mathlib

English

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

Русский

t ∈ ∂ 𝒜 тогда и только тогда, когда существует s ∈ 𝒜, such that t ⊆ s и #(s \\ t) = 1.

LaTeX

$$$$ t \\in ∂ 𝒜 \\iff \\exists s \\in 𝒜, t \\subseteq s \\land |s \\setminus t| = 1 $$$$

Lean4

/-- `t` is in the shadow of `𝒜` iff we can add an element to it so that the resulting finset is in
`𝒜`. -/
theorem mem_shadow_iff_insert_mem : t ∈ ∂ 𝒜 ↔ ∃ a ∉ t, insert a t ∈ 𝒜 :=
  by
  simp_rw [mem_shadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]
  aesop

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