ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : { x // x ∈ S i }) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, ↑(sumAddHom fun i => AddSubmonoid.subtype (S i)) f = x) ↔ ∃ f, (sum f fun i xi => ↑xi) = x
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : { x // x ∈ S i }) → Decidable (x ≠ 0)
x : γ
⊢ x ∈ iSup S ↔ ∃ f, (sum f fun i xi => ↑xi) = x
rw [AddSubmonoid.mem_iSup_iff_exists_dfinsupp]
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : { x // x ∈ S i }) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (sum f fun x => ↑(AddSubmonoid.subtype (S x))) = x) ↔ ∃ f, (sum f fun i xi => ↑xi) = x
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : { x // x ∈ S i }) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, ↑(sumAddHom fun i => AddSubmonoid.subtype (S i)) f = x) ↔ ∃ f, (sum f fun i xi => ↑xi) = x
simp_rw [sumAddHom_apply]
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : { x // x ∈ S i }) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (sum f fun x => ↑(AddSubmonoid.subtype (S x))) = x) ↔ ∃ f, (sum f fun i xi => ↑xi) = x
rfl