[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f✝ : ι →₀ α
i✝ : ι
a : α
f : ι →₀ α
i : ι
⊢ i ∈ f.support ↔ (fun i => {↑f i}) i ≠ 0
[PROOFSTEP]
rw [← not_iff_not, not_mem_support_iff, not_ne_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f✝ : ι →₀ α
i✝ : ι
a : α
f : ι →₀ α
i : ι
⊢ ↑f i = 0 ↔ (fun i => {↑f i}) i = 0
[PROOFSTEP]
exact singleton_injective.eq_iff.symm
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Zero α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
f✝ g✝ : ι →₀ α
i✝ : ι
a : α
f g : ι →₀ α
i : ι
⊢ i ∈ f.support ∪ g.support ↔ (fun i => Icc (↑f i) (↑g i)) i ≠ 0
[PROOFSTEP]
rw [mem_union, ← not_iff_not, not_or, not_mem_support_iff, not_mem_support_iff, not_ne_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Zero α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
f✝ g✝ : ι →₀ α
i✝ : ι
a : α
f g : ι →₀ α
i : ι
⊢ ↑f i = 0 ∧ ↑g i = 0 ↔ (fun i => Icc (↑f i) (↑g i)) i = 0
[PROOFSTEP]
exact Icc_eq_singleton_iff.symm
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f✝ g✝ f g x : ι →₀ α
⊢ x ∈ (fun f g => Finset.finsupp (f.support ∪ g.support) ↑(rangeIcc f g)) f g ↔ f ≤ x ∧ x ≤ g
[PROOFSTEP]
refine' (mem_finsupp_iff_of_support_subset <| Finset.subset_of_eq <| rangeIcc_support _ _).trans _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f✝ g✝ f g x : ι →₀ α
⊢ (∀ (i : ι), ↑x i ∈ ↑(rangeIcc f g) i) ↔ f ≤ x ∧ x ≤ g
[PROOFSTEP]
simp_rw [mem_rangeIcc_apply_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f✝ g✝ f g x : ι →₀ α
⊢ (∀ (i : ι), ↑f i ≤ ↑x i ∧ ↑x i ≤ ↑g i) ↔ f ≤ x ∧ x ≤ g
[PROOFSTEP]
exact forall_and
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (Icc f g) = ∏ i in f.support ∪ g.support, card (Icc (↑f i) (↑g i))
[PROOFSTEP]
simp_rw [Icc_eq, card_finsupp, coe_rangeIcc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (Ico f g) = ∏ i in f.support ∪ g.support, card (Icc (↑f i) (↑g i)) - 1
[PROOFSTEP]
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (Ioc f g) = ∏ i in f.support ∪ g.support, card (Icc (↑f i) (↑g i)) - 1
[PROOFSTEP]
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (Ioo f g) = ∏ i in f.support ∪ g.support, card (Icc (↑f i) (↑g i)) - 2
[PROOFSTEP]
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Lattice α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (uIcc f g) = ∏ i in f.support ∪ g.support, card (uIcc (↑f i) (↑g i))
[PROOFSTEP]
rw [← support_inf_union_support_sup]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Lattice α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (uIcc f g) = ∏ i in (f ⊓ g).support ∪ (f ⊔ g).support, card (uIcc (↑f i) (↑g i))
[PROOFSTEP]
exact card_Icc (_ : ι →₀ α) _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyOrderedAddMonoid α
inst✝ : LocallyFiniteOrder α
f : ι →₀ α
⊢ card (Iic f) = ∏ i in f.support, card (Iic (↑f i))
[PROOFSTEP]
classical simp_rw [Iic_eq_Icc, card_Icc, Finsupp.bot_eq_zero, support_zero, empty_union, zero_apply, bot_eq_zero]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyOrderedAddMonoid α
inst✝ : LocallyFiniteOrder α
f : ι →₀ α
⊢ card (Iic f) = ∏ i in f.support, card (Iic (↑f i))
[PROOFSTEP]
simp_rw [Iic_eq_Icc, card_Icc, Finsupp.bot_eq_zero, support_zero, empty_union, zero_apply, bot_eq_zero]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyOrderedAddMonoid α
inst✝ : LocallyFiniteOrder α
f : ι →₀ α
⊢ card (Iio f) = ∏ i in f.support, card (Iic (↑f i)) - 1
[PROOFSTEP]
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
