mem_upShadow_iff — Mathlib

English

An element t belongs to the upper shadow ∂⁺ 𝒜 if and only if there exist s ∈ 𝒜 and a ∉ s with insert a s = t.

Русский

Элемент t принадлежит верхней тени ∂⁺ 𝒜 тогда и только тогда, когда существуют s ∈ 𝒜 и a ∉ s, такие что insert a s = t.

LaTeX

$$$ t ∈ ∂⁺ 𝒜 \iff ∃ s ∈ 𝒜, ∃ a \notin s, insert a s = t $$$

Lean4

/-- `t` is in the upper shadow of `𝒜` iff there is a `s ∈ 𝒜` from which we can remove one element
to get `t`. -/
theorem mem_upShadow_iff : t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t := by
  simp_rw [upShadow, mem_sup, mem_image, mem_compl]

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