memberSubfamily_image_erase — Mathlib

English

If we erase a from every member of 𝒜 and then take the subfamily consisting of a, the result is empty: (𝒜.image erase a).memberSubfamily a = ∅.

Русский

Если из каждого элемента 𝒜 удалить элемент a и затем взять подсемейство элементов, содержащих a, получим пустое множество.

LaTeX

$$$ (\\mathcal{A}.image( erase\\ a)).{\\rm memberSubfamily}\\ a = \\emptyset $$$

Lean4

@[simp]
theorem memberSubfamily_image_erase : (𝒜.image (erase · a)).memberSubfamily a = ∅ := by
  simp [eq_empty_iff_forall_notMem, (ne_of_mem_of_not_mem' (mem_insert_self _ _) (notMem_erase _ _)).symm]

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