@[simp]

theorem Sigma.fst_comp_mk_eq_id {α : Type u_1} {β : α → Type u_2} {f : (i : α) → β i} : ((fun (x : (i : α) × β i) => x.fst) ∘ fun (i : α) => ⟨i, f i⟩) = fun (i : α) => i

def Sigma.toProd {α : Type u_1} {β : Type u_2} (x : (_ : α) × β) : α × β

Equations

• x.toProd = (x.fst, x.snd)

@[simp]

theorem Sigma.prod_to_sigma_comp_sigma_to_prod {α : Type u_1} {β : Type u_2} : toProd ∘ Prod.toSigma = id

@[simp]

theorem Sigma.sigma_to_prod_comp_prod_to_sigma {α : Type u_1} {β : Type u_2} : Prod.toSigma ∘ toProd = id

theorem Sigma.toProd_inj {α : Type u_1} {β : Type u_2} {x y : (_ : α) × β} (h : x.toProd = y.toProd) : x = y

@[simp]

theorem Sigma.toProd_eq_toProd {α : Type u_1} {β : Type u_2} {x y : (_ : α) × β} : x.toProd = y.toProd ↔ x = y

@[simp]

theorem Sigma.injective_toProd {α : Type u_1} {β : Type u_2} : Function.Injective toProd

@[simp]

theorem Option.map_sigma_toProd_eq_iff {α : Type u_1} {β : Type u_2} {ma mb : Option ((_ : α) × β)} : Option.map Sigma.toProd ma = Option.map Sigma.toProd mb ↔ ma = mb

@[simp]

theorem List.map_sigma_toProd_eq_iff {α : Type u_1} {β : Type u_2} {xs ys : List ((_ : α) × β)} : map Sigma.toProd xs = map Sigma.toProd ys ↔ xs = ys

theorem List.ind_pair_sigma {α : Type u_1} {β : Type u_2} {P : List (α × β) → Prop} (h : ∀ (xs : List ((_ : α) × β)), P (map Sigma.toProd xs)) (xs : List (α × β)) : P xs

@[simp]

theorem Sigma.fst_eq_fst_and_eq_iff {α : Type u_1} {β : α → Type u_2} {x y : (i : α) × β i} : x.fst = y.fst ∧ x = y ↔ x = y

@[simp]

theorem Sigma.foall_nd {α : Type u_1} {β : Type u_2} {p : (_ : α) × β → Prop} : (∀ (x : (_ : α) × β), p x) ↔ ∀ (x : α) (y : β), p ⟨x, y⟩