mathlib docs: data.sigma.basic

source

@[instance]

def sigma.inhabited {α : Type u_1} {β : α → Type u_4} [inhabited α] [inhabited (β (default α))] :

inhabited (sigma β)

Equations

sigma.inhabited = {default := ⟨default α _inst_1, default (β (default α)) _inst_2⟩}

source

@[instance]

def sigma.decidable_eq {α : Type u_1} {β : α → Type u_4} [h₁ : decidable_eq α] [h₂ : Π (a : α), decidable_eq (β a)] :

decidable_eq (sigma β)

Equations

sigma.decidable_eq ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ = sigma.decidable_eq._match_1 a₁ b₁ a₂ b₂ (h₁ a₁ a₂)
sigma.decidable_eq._match_1 a b₁ a b₂ (is_true _) = sigma.decidable_eq._match_2 a b₁ b₂ (h₂ a b₁ b₂)
sigma.decidable_eq._match_1 a₁ _x a₂ _x_1 (is_false n) = is_false _
sigma.decidable_eq._match_2 a b b (is_true _) = is_true _
sigma.decidable_eq._match_2 a b₁ b₂ (is_false n) = is_false _

source

@[simp, nolint]

theorem sigma.mk.inj_iff {α : Type u_1} {β : α → Type u_4} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :

⟨a₁, b₁⟩ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ b₁ == b₂

source

@[simp]

theorem sigma.eta {α : Type u_1} {β : α → Type u_4} (x : Σ (a : α), β a) :

⟨x.fst, x.snd⟩ = x

source

@[ext]

theorem sigma.ext {α : Type u_1} {β : α → Type u_4} {x₀ x₁ : sigma β} (h₀ : x₀.fst = x₁.fst) (h₁ : x₀.snd == x₁.snd) :

x₀ = x₁

source

theorem sigma.ext_iff {α : Type u_1} {β : α → Type u_4} {x₀ x₁ : sigma β} :

x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ x₀.snd == x₁.snd

source

@[simp]

theorem sigma.forall {α : Type u_1} {β : α → Type u_4} {p : (Σ (a : α), β a) → Prop} :

(∀ (x : Σ (a : α), β a), p x) ↔ ∀ (a : α) (b : β a), p ⟨a, b⟩

source

@[simp]

theorem sigma.exists {α : Type u_1} {β : α → Type u_4} {p : (Σ (a : α), β a) → Prop} :

(∃ (x : Σ (a : α), β a), p x) ↔ ∃ (a : α) (b : β a), p ⟨a, b⟩

source

def sigma.map {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁ → Type u_5} {β₂ : α₂ → Type u_6} (f₁ : α₁ → α₂) (f₂ : Π (a : α₁), β₁ a → β₂ (f₁ a)) (x : sigma β₁) :

sigma β₂

Map the left and right components of a sigma

Equations

sigma.map f₁ f₂ x = ⟨f₁ x.fst, f₂ x.fst x.snd⟩

source

theorem sigma_mk_injective {α : Type u_1} {β : α → Type u_4} {i : α} :

function.injective (sigma.mk i)

source

theorem function.injective.sigma_map {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁ → Type u_5} {β₂ : α₂ → Type u_6} {f₁ : α₁ → α₂} {f₂ : Π (a : α₁), β₁ a → β₂ (f₁ a)} (h₁ : function.injective f₁) (h₂ : ∀ (a : α₁), function.injective (f₂ a)) :

function.injective (sigma.map f₁ f₂)

source

theorem function.surjective.sigma_map {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁ → Type u_5} {β₂ : α₂ → Type u_6} {f₁ : α₁ → α₂} {f₂ : Π (a : α₁), β₁ a → β₂ (f₁ a)} (h₁ : function.surjective f₁) (h₂ : ∀ (a : α₁), function.surjective (f₂ a)) :

function.surjective (sigma.map f₁ f₂)

source

def sigma.curry {α : Type u_1} {β : α → Type u_4} {γ : Π (a : α), β a → Type u_2} (f : Π (x : sigma β), γ x.fst x.snd) (x : α) (y : β x) :

γ x y

Interpret a function on Σ x : α, β x as a dependent function with two arguments.

Equations

sigma.curry f x y = f ⟨x, y⟩

source

def sigma.uncurry {α : Type u_1} {β : α → Type u_4} {γ : Π (a : α), β a → Type u_2} (f : Π (x : α) (y : β x), γ x y) (x : sigma β) :

γ x.fst x.snd

Interpret a dependent function with two arguments as a function on Σ x : α, β x

Equations

sigma.uncurry f x = f x.fst x.snd

source

@[simp]

def prod.to_sigma {α : Type u_1} {β : Type u_2} (a : α × β) :

Σ (_x : α), β

Convert a product type to a Σ-type.

Equations

(x, y).to_sigma = ⟨x, y⟩

source

@[simp]

theorem prod.fst_to_sigma {α : Type u_1} {β : Type u_2} (x : α × β) :

x.to_sigma.fst = x.fst

source

@[simp]

theorem prod.snd_to_sigma {α : Type u_1} {β : Type u_2} (x : α × β) :

x.to_sigma.snd = x.snd

source

def psigma.elim {α : Sort u_1} {β : α → Sort u_2} {γ : Sort u_3} (f : Π (a : α), β a → γ) (a : psigma β) :

γ

Nondependent eliminator for psigma.

Equations

psigma.elim f a = a.cases_on f

source

@[simp]

theorem psigma.elim_val {α : Sort u_1} {β : α → Sort u_2} {γ : Sort u_3} (f : Π (a : α), β a → γ) (a : α) (b : β a) :

psigma.elim f ⟨a, b⟩ = f a b

source

@[instance]

def psigma.inhabited {α : Sort u_1} {β : α → Sort u_2} [inhabited α] [inhabited (β (default α))] :

inhabited (psigma β)

Equations

psigma.inhabited = {default := ⟨default α _inst_1, default (β (default α)) _inst_2⟩}

source

@[instance]

def psigma.decidable_eq {α : Sort u_1} {β : α → Sort u_2} [h₁ : decidable_eq α] [h₂ : Π (a : α), decidable_eq (β a)] :

decidable_eq (psigma β)

Equations

psigma.decidable_eq ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ = psigma.decidable_eq._match_1 a₁ b₁ a₂ b₂ (h₁ a₁ a₂)
psigma.decidable_eq._match_1 a b₁ a b₂ (is_true _) = psigma.decidable_eq._match_2 a b₁ b₂ (h₂ a b₁ b₂)
psigma.decidable_eq._match_1 a₁ _x a₂ _x_1 (is_false n) = is_false _
psigma.decidable_eq._match_2 a b b (is_true _) = is_true _
psigma.decidable_eq._match_2 a b₁ b₂ (is_false n) = is_false _

source

theorem psigma.mk.inj_iff {α : Sort u_1} {β : α → Sort u_2} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :

⟨a₁, b₁⟩ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ b₁ == b₂

source

@[ext]

theorem psigma.ext {α : Sort u_1} {β : α → Sort u_2} {x₀ x₁ : psigma β} (h₀ : x₀.fst = x₁.fst) (h₁ : x₀.snd == x₁.snd) :

x₀ = x₁

source

theorem psigma.ext_iff {α : Sort u_1} {β : α → Sort u_2} {x₀ x₁ : psigma β} :

x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ x₀.snd == x₁.snd

source

def psigma.map {α₁ : Sort u_3} {α₂ : Sort u_4} {β₁ : α₁ → Sort u_5} {β₂ : α₂ → Sort u_6} (f₁ : α₁ → α₂) (f₂ : Π (a : α₁), β₁ a → β₂ (f₁ a)) (a : psigma β₁) :

psigma β₂

Map the left and right components of a sigma

Equations

psigma.map f₁ f₂ ⟨a, b⟩ = ⟨f₁ a, f₂ a b⟩