mem_iSup_iff_exists_dfinsupp' — Mathlib

English

A variant with unfolded right-hand side: membership in iSup S is equivalent to an existential dfinsupp f with a certain equality to x after sumAddHom.

Русский

Вариант с полным раскрытием RHS: принадлежность x iSup S эквивалентна существованию dfinsupp f, для которого выполняется требуемое равенство.

LaTeX

$$$ x \in \iSup S \iff \exists f:\Pi₀ i, S_i, (\mathrm{sumAddHom}(\text{fun } i => (S_i).subtype) f) = x$$$

Lean4

/-- A variant of `AddSubmonoid.mem_iSup_iff_exists_dfinsupp` with the RHS fully unfolded. -/
theorem mem_iSup_iff_exists_dfinsupp' [AddCommMonoid γ] (S : ι → AddSubmonoid γ) [∀ (i) (x : S i), Decidable (x ≠ 0)]
    (x : γ) : x ∈ iSup S ↔ ∃ f : Π₀ i, S i, (f.sum fun _ xi => ↑xi) = x :=
  by
  rw [AddSubmonoid.mem_iSup_iff_exists_dfinsupp]
  simp_rw [sumAddHom_apply]
  rfl

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