def iProd {ι : Type u_2} {x : ι → Type u_5} (y : (i : ι) → Set (x i)) : Set ((i : ι) → x i)

Equations

• iProd y = {f : (i : ι) → x i | ∀ (i : ι), f i ∈ y i}

@[simp]

def mem_iProd_iff {ι : Type u_2} {x : ι → Type u_5} {y : (i : ι) → Set (x i)} {a : (i : ι) → x i} : a ∈ iProd y ↔ ∀ (i : ι), a i ∈ y i

Equations

• ⋯ = ⋯

def iProdBuilder : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def elabiProdBuilder : Lean.Elab.Term.TermElab

Equations

• One or more equations did not get rendered due to their size.

def iProd.unexpander : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

theorem Set.Product.subset_iProd_image_proj {ι : Type u_2} {x : ι → Type u_5} {a : Set ((i : ι) → x i)} : a ⊆ Πˢ i : ι, (fun (s : (i : ι) → x i) => s i) '' a

def Set.Product.iProd_to_prod {ι : Type u_2} {x : ι → Type u_5} {y : (i : ι) → Set (x i)} (p : ↥(iProd y)) (i : ι) : ↥(y i)

Equations

• Set.Product.iProd_to_prod p i = ⟨p.val i, ⋯⟩

def Set.Product.prod_to_iProd {ι : Type u_2} {x : ι → Type u_5} {y : (i : ι) → Set (x i)} (p : (i : ι) → ↥(y i)) : ↥(iProd y)

Equations

• Set.Product.prod_to_iProd p = ⟨fun (i : ι) => (p i).val, ⋯⟩

theorem Set.Product.prod_to_iProd_inverse {ι : Type u_2} {x : ι → Type u_5} {y : (i : ι) → Set (x i)} : Function.IsInverseOf Set.Product.iProd_to_prod Set.Product.prod_to_iProd

@[simp]

theorem Set.Product.iProd_univ {ι : Type u_7} {x : ι → Type u_9} : Πˢ i : ι, Set.univ = Set.univ

theorem Set.Product.iProd_iUnion_distrib {ι : Type u_7} {ι' : ι → Type u_8} {x : ι → Type u_9} {y : (i : ι) → ι' i → Set (x i)} : Πˢ i : ι, ⋃ i' : ι' i, y i i' = ⋃ i'' : (i : ι) → ι' i, Πˢ i : ι, y i (i'' i)

theorem Set.Product.iProd_iInter_distrib {ι : Type u_7} {ι' : ι → Type u_8} {x : ι → Type u_9} {y : (i : ι) → ι' i → Set (x i)} (ne : ∀ (i : ι), Nonempty (ι' i)) : Πˢ i : ι, ⋂ i' : ι' i, y i i' = ⋂ i'' : (i : ι) → ι' i, Πˢ i : ι, y i (i'' i)

theorem Set.Product.iProd_iInter_two_distrib {ι : Type u_7} {ι' : Type u_10} {x : ι → Type u_11} {y : (i : ι) → ι' → Set (x i)} : ⋂ i' : ι', Πˢ i : ι, y i i' = Πˢ i : ι, ⋂ i' : ι', y i i'

theorem Set.Product.iProd_inter_distrib {ι : Type u_7} {x : ι → Type u_10} {y y' : (i : ι) → Set (x i)} : (Πˢ i : ι, y i) ∩ Πˢ i : ι, y' i = Πˢ i : ι, y i ∩ y' i

theorem Set.Product.iInter_prod_distrib {ι : Type u_7} {α : Type u_10} {y y' : ι → Set α} : (⋂ i : ι, y i).prod (⋂ i : ι, y' i) = ⋂ i : ι, (y i).prod (y' i)

theorem Set.Product.iProd_eq_iInter_preimage {ι : Type u_7} {x : ι → Type u_9} {y : (i : ι) → Set (x i)} : Πˢ i : ι, y i = ⋂ i : ι, (fun (f : (i : ι) → x i) => f i) ⁻¹' y i

theorem Set.Set.iProd_isCovering {ι : Type u_7} {ι' : ι → Type u_8} {x : ι → Type u_9} {y : (i : ι) → ι' i → Set (x i)} (h : ∀ (i : ι), Set.IsCovering (y i)) : Set.IsCovering fun (i' : (i : ι) → ι' i) => Πˢ i : ι, y i (i' i)

theorem Set.Set.iProd_disjoint {ι : Type u_7} {ι' : ι → Type u_8} {x : ι → Type u_9} {y : (i : ι) → ι' i → Set (x i)} (h : ∀ (i : ι), Set.Disjoint (y i)) : Set.Disjoint fun (i' : (i : ι) → ι' i) => Πˢ i : ι, y i (i' i)

theorem Set.Set.iProd_isPartition {ι : Type u_7} {ι' : ι → Type u_8} {x : ι → Type u_9} {y : (i : ι) → ι' i → Set (x i)} (h : ∀ (i : ι), Set.IsPartition (y i)) : Set.IsPartition fun (i' : (i : ι) → ι' i) => Πˢ i : ι, y i (i' i)