attach — Mathlib

English

If s is a Finset, then attaching it and composing with f preserves pairwise disjointness: s.attach toSet is pairwiseDisjoint with f ∘ Subtype.val.

Русский

Если s — Finset, прикрепление его кSet сохраняет попарную непересекаемость: s.attach в Set имеет свойство PairwiseDisjoint (f ∘ Subtype.val).

LaTeX

$$hs : (s : Set ι).PairwiseDisjoint f → (s.attach : Set { x // x ∈ s }).PairwiseDisjoint (f ∘ Subtype.val)$$

Lean4

theorem attach (hs : (s : Set ι).PairwiseDisjoint f) :
    (s.attach : Set { x // x ∈ s }).PairwiseDisjoint (f ∘ Subtype.val) := fun i _ j _ hij =>
  hs i.2 j.2 <| mt Subtype.ext hij

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