covBy_iff_exists_erase — Mathlib

English

For Finsets s and t, s ⋖ t if and only if there exists an element a ∈ t such that t.erase a = s.

Русский

Для Finset s и t: s ⋖ t тогда и только тогда, когда существует элемент a ∈ t, такой что t.erase a = s.

LaTeX

$$$ s \ CovBy t \iff \exists a \in t, t.erase(a) = s $$$

Lean4

theorem covBy_iff_exists_erase : s ⋖ t ↔ ∃ a ∈ t, t.erase a = s := by
  simp only [← coe_covBy_coe, Set.covBy_iff_exists_sdiff_singleton, ← coe_inj, coe_erase, mem_coe]

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