exists_subset_of_mem_upShadow — Mathlib

English

If t is in the upper shadow ∂⁺ 𝒜, then there exists s ∈ 𝒜 with s ⊆ t.

Русский

Если t принадлежит верхней тени ∂⁺ 𝒜, то существует s ∈ 𝒜 such that s ⊆ t.

LaTeX

$$$ t ∈ ∂⁺ 𝒜 \Rightarrow \exists s ∈ 𝒜, s ⊆ t $$$

Lean4

/-- Being in the upper shadow of `𝒜` means we have a superset in `𝒜`. -/
theorem exists_subset_of_mem_upShadow (hs : s ∈ ∂⁺ 𝒜) : ∃ t ∈ 𝒜, t ⊆ s :=
  let ⟨t, ht, hts, _⟩ := mem_upShadow_iff_exists_mem_card_add_one.1 hs
  ⟨t, ht, hts⟩

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