erase_mem_shadow — Mathlib

English

If s ∈ 𝒜 and a ∈ s, then erase s a ∈ ∂ 𝒜 (alternative presentation of the shadow criterion).

Русский

Если s ∈ 𝒜 и a ∈ s, то erase s a ∈ ∂ 𝒜 (альтернативное представление критерия тени).

LaTeX

$$$$ \\text{If } s \\in 𝒜 \\text{ and } a \\in s, \\ \\mathrm{erase}(s,a) \\in ∂ 𝒜 $$$$

Lean4

theorem erase_mem_shadow (hs : s ∈ 𝒜) (ha : a ∈ s) : erase s a ∈ ∂ 𝒜 :=
  mem_shadow_iff.2 ⟨s, hs, a, ha, rfl⟩

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