supIndep_attach — Mathlib

English

The SupIndep property is preserved when attaching a Finset to a function: (s.attach.SupIndep (fun a => f a)) is equivalent to s.SupIndep f.

Русский

Свойство SupIndep сохраняется при присоединении: (s.attach.SupIndep (fun a => f a)) эквивалентно s.SupIndep f.

LaTeX

$$$(s.attach.SupIndep fun a => f a) \\iff s.SupIndep f$$$

Lean4

@[simp]
theorem supIndep_attach : (s.attach.SupIndep fun a => f a) ↔ s.SupIndep f := by
  simpa [Finset.attach_map_val] using (supIndep_map (s := s.attach) (g := .subtype _)).symm

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