memberSubfamily — Mathlib

English

Image of the members of 𝒜 that contain a, after removing a from them.

Русский

Образ элементов 𝒜, которые содержат a, после удаления a из них.

LaTeX

$$$\operatorname{memberSubfamily}(a, 𝒜) = \{ \operatorname{erase}(s, a) \mid s \in 𝒜 \text{ and } a \in s \ \}$$$

Lean4

/-- Image of the elements of `𝒜` which contain `a` under removing `a`. Finsets that do not contain
`a` such that `insert a s ∈ 𝒜`. -/
def memberSubfamily (a : α) (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
  {s ∈ 𝒜 | a ∈ s}.image fun s => erase s a

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