α : Type u_1
ι : Sort u_2
κ : ι → Sort ?u.406
A B : Set (Finset α)
r : ℕ
f : ι → Set (Finset α)
⊢ (∀ ⦃x : Finset α⦄ (x_1 : ι), x ∈ f x_1 → card x = r) ↔ ∀ (i : ι) ⦃x : Finset α⦄, x ∈ f i → card x = r
α : Type u_1
ι : Sort u_2
κ : ι → Sort ?u.406
A B : Set (Finset α)
r : ℕ
f : ι → Set (Finset α)
⊢ Sized r (⋃ (i : ι), f i) ↔ ∀ (i : ι), Sized r (f i)
simp_rw [Set.Sized, Set.mem_iUnion, forall_exists_index]
no goals
α : Type u_1
ι : Sort u_2
κ : ι → Sort ?u.406
A B : Set (Finset α)
r : ℕ
f : ι → Set (Finset α)
⊢ (∀ ⦃x : Finset α⦄ (x_1 : ι), x ∈ f x_1 → card x = r) ↔ ∀ (i : ι) ⦃x : Finset α⦄, x ∈ f i → card x = r
exact forall_swap