English
Let s be a finite set and g an embedding ι' → ι. The SupIndep property is preserved by map: (s.map g).SupIndep f is equivalent to s.SupIndep (f ∘ g).
Русский
Пусть s — конечное множество, а отображение g: ι'↪ ι. Свойство SupIndep сохраняется под отображением: (s.map g).SupIndep f эквивалентно s.SupIndep (f ∘ g).
LaTeX
$$$(s.map\\ g).SupIndep\\ f \\iff\\ s.SupIndep (f \\circ g)$$$
Lean4
theorem supIndep_map {s : Finset ι'} {g : ι' ↪ ι} : (s.map g).SupIndep f ↔ s.SupIndep (f ∘ g) :=
by
refine ⟨fun hs t ht i hi hit => ?_, fun hs => ?_⟩
· rw [← sup_map]
exact hs (map_subset_map.2 ht) ((mem_map' _).2 hi) (by rwa [mem_map'])
·
classical
rw [map_eq_image]
exact hs.image
