English
For a directed lattice and an injOn condition, iSupIndep f is equivalent to supIndep on all finite index sets.
Русский
Для направленной решётки и условия инъекции InjOn, iSupIndep f эквивалентно SupIndep на всех конечных подмножествах индексов.
LaTeX
$$$ iSupIndep f \iff \forall s : Finset ι, s.SupIndep f $$$
Lean4
theorem iSupIndep_iff_supIndep_of_injOn {ι : Type*} {f : ι → α} (hf : InjOn f {i | f i ≠ ⊥}) :
iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f :=
by
refine ⟨fun h ↦ h.supIndep', fun h ↦ iSupIndep_def'.mpr fun i ↦ ?_⟩
simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
intro s hs
classical
rw [← Finset.sup_erase_bot]
set t := s.erase ⊥
replace hf : InjOn f (f ⁻¹' t) := fun i hi j _ hij ↦ by refine hf ?_ ?_ hij <;> aesop (add norm simp [t])
have : (Finset.erase (insert i (t.preimage _ hf)) i).image f = t :=
by
ext a
simp only [Finset.mem_preimage, Finset.mem_erase, ne_eq, Finset.erase_insert_eq_erase, Finset.mem_image, t]
refine ⟨by aesop, fun ⟨ha, has⟩ ↦ ?_⟩
obtain ⟨j, hj, rfl⟩ := hs has
exact ⟨j, ⟨hj, ha, has⟩, rfl⟩
rw [← this, Finset.sup_image]
specialize h (insert i (t.preimage _ hf))
rw [Finset.supIndep_iff_disjoint_erase] at h
exact h i (Finset.mem_insert_self i _)
