mathlib documentation

data.sigma.basic

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

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

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 _
@[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₂

@[simp]
theorem sigma.eta {α : Type u_1} {β : α → Type u_4} (x : Σ (a : α), β a) :
x.fst, x.snd = x

@[ext]
theorem sigma.ext {α : Type u_1} {β : α → Type u_4} {x₀ x₁ : sigma β} :
x₀.fst = x₁.fstx₀.snd == x₁.sndx₀ = x₁

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

@[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⟩

@[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⟩

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

Map the left and right components of a sigma

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

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

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

def sigma.curry {α : Type u_1} {β : α → Type u_4} {γ : Π (a : α), β aType 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
def sigma.uncurry {α : Type u_1} {β : α → Type u_4} {γ : Π (a : α), β aType 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
@[simp]
def prod.to_sigma {α : Type u_1} {β : Type u_2} :
α × β(Σ (_x : α), β)

Convert a product type to a Σ-type.

Equations
@[simp]
theorem prod.fst_to_sigma {α : Type u_1} {β : Type u_2} (x : α × β) :

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

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

Nondependent eliminator for psigma.

Equations
@[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

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

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

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 _
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₂

@[ext]
theorem psigma.ext {α : Sort u_1} {β : α → Sort u_2} {x₀ x₁ : psigma β} :
x₀.fst = x₁.fstx₀.snd == x₁.sndx₀ = x₁

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

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

Map the left and right components of a sigma

Equations