nonMemberSubfamily_image_insert — Mathlib

English

If we take the image of a finitary family 𝒜 under the operation insert a, the subfamily not containing a is empty: (𝒜.image insert a).nonMemberSubfamily a = ∅.

Русский

Если взять образ семейства 𝒜 под операцией вставки a, то подсемейство без a пусто: (𝒜.image insert a).nonMemberSubfamily a = ∅.

LaTeX

$$$ (\\mathcal{A}.image( insert\\ a)).nonMemberSubfamily\\ a = \\emptyset $$$

Lean4

@[simp]
theorem nonMemberSubfamily_image_insert : (𝒜.image <| insert a).nonMemberSubfamily a = ∅ := by
  simp [eq_empty_iff_forall_notMem]

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