English
An equivalent formulation of the finite witness property for iSup in Submodule contexts.
Русский
Эквивалентная формулировка свойства существования конечного поднабора для iSup в контекстах Submodule.
LaTeX
$$Iff (m ∈ ⨆ i, p i) (∃ s : Finset, m ∈ ⨆ i ∈ s, p i)$$
Lean4
theorem mem_sSup_iff_exists_finset {S : Set (Submodule R M)} {m : M} :
m ∈ sSup S ↔ ∃ s : Finset (Submodule R M), ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i :=
by
rw [sSup_eq_iSup, iSup_subtype', Submodule.mem_iSup_iff_exists_finset]
refine
⟨fun ⟨s, hs⟩ ↦ ⟨s.map (Function.Embedding.subtype S), ?_, ?_⟩, fun ⟨s, hsS, hs⟩ ↦
⟨s.preimage (↑) Subtype.coe_injective.injOn, ?_⟩⟩
· simpa using fun x _ ↦ x.property
· suffices m ∈ ⨆ (i) (hi : i ∈ S) (_ : ⟨i, hi⟩ ∈ s), i by simpa
rwa [iSup_subtype']
· have : ⨆ (i) (_ : i ∈ S ∧ i ∈ s), i = ⨆ (i) (_ : i ∈ s), i := by convert rfl; aesop
simpa only [Finset.mem_preimage, iSup_subtype, iSup_and', this]
