exists_subset_of_mem_shadow — Mathlib

English

If t belongs to the shadow ∂𝒜, then there exists some s in 𝒜 such that t is a subset of s.

Русский

Если t принадлежит теням ∂𝒜, то существует такое s ∈ 𝒜, что t ⊆ s.

LaTeX

$$$ t \in ∂ 𝒜 \; \Rightarrow \; \exists s \in 𝒜,\; t \subseteq s $$$

Lean4

/-- Being in the shadow of `𝒜` means we have a superset in `𝒜`. -/
theorem exists_subset_of_mem_shadow (hs : t ∈ ∂ 𝒜) : ∃ s ∈ 𝒜, t ⊆ s :=
  let ⟨t, ht, hst⟩ := mem_shadow_iff_exists_mem_card_add_one.1 hs
  ⟨t, ht, hst.1⟩

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