[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b x : (i : ι) → α i
⊢ x ∈ (fun a b => piFinset fun i => Icc (a i) (b i)) a b ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
simp_rw [mem_piFinset, mem_Icc, le_def, forall_and]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ Finset.card (Ico a b) = ∏ i : ι, Finset.card (Icc (a i) (b i)) - 1
[PROOFSTEP]
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ Finset.card (Ioc a b) = ∏ i : ι, Finset.card (Icc (a i) (b i)) - 1
[PROOFSTEP]
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ Finset.card (Ioo a b) = ∏ i : ι, Finset.card (Icc (a i) (b i)) - 2
[PROOFSTEP]
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
b✝ b x : (i : ι) → α i
⊢ x ∈ (fun b => piFinset fun i => Iic (b i)) b ↔ x ≤ b
[PROOFSTEP]
simp_rw [mem_piFinset, mem_Iic, le_def]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
b : (i : ι) → α i
⊢ Finset.card (Iio b) = ∏ i : ι, Finset.card (Iic (b i)) - 1
[PROOFSTEP]
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a✝ a x : (i : ι) → α i
⊢ x ∈ (fun a => piFinset fun i => Ici (a i)) a ↔ a ≤ x
[PROOFSTEP]
simp_rw [mem_piFinset, mem_Ici, le_def]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a : (i : ι) → α i
⊢ Finset.card (Ioi a) = ∏ i : ι, Finset.card (Ici (a i)) - 1
[PROOFSTEP]
rw [card_Ioi_eq_card_Ici_sub_one, card_Ici]
