mem_iSup_iff_exists_finsupp — Mathlib

English

Equivalence between membership in the iSup and existence of a dfinsupp witnessing it.

Русский

Эквивалентность принадлежности к iSup и существование dfinsupp, подтверждающего это.

LaTeX

$$$x \\in iSup p \\;\\iff\\; \\exists f : Π₀ i, p i, \\; \\mathrm{lsum}\\; (..)\\; f = x$$$

Lean4

theorem mem_iSup_iff_exists_finsupp (p : ι → Submodule R N) (x : N) :
    x ∈ iSup p ↔ ∃ (f : ι →₀ N), (∀ i, f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x := by
  classical
  rw [mem_iSup_iff_exists_dfinsupp']
  refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩
  rintro ⟨f, hf, rfl⟩
  refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩
  · ext; simp [mk_eq_zero]
  · simp [Finsupp.mem_support_iff.mp hi]

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