@[instance]
def
sigma.inhabited
{α : Type u_1}
{β : α → Type u_2}
[inhabited α]
[inhabited (β (inhabited.default α))] :
Equations
- sigma.inhabited = {default := ⟨inhabited.default α _inst_1, inhabited.default (β (inhabited.default α)) _inst_2⟩}
@[instance]
def
sigma.decidable_eq
{α : Type u_1}
{β : α → Type u_2}
[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₂ (decidable.is_true _) = sigma.decidable_eq._match_2 a b₁ b₂ (h₂ a b₁ b₂)
- sigma.decidable_eq._match_1 a₁ _x a₂ _x_1 (decidable.is_false n) = decidable.is_false _
- sigma.decidable_eq._match_2 a b b (decidable.is_true _) = decidable.is_true _
- sigma.decidable_eq._match_2 a b₁ b₂ (decidable.is_false n) = decidable.is_false _
@[simp]
@[simp]
theorem
function.injective.sigma_map
{α₁ : Type u_3}
{α₂ : Type u_4}
{β₁ : α₁ → 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_3}
{α₂ : Type u_4}
{β₁ : α₁ → 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
psigma.elim
{α : Sort u_1}
{β : α → Sort u_2}
{γ : Sort u_3} :
(Π (a : α), β a → γ) → psigma β → γ
Nondependent eliminator for psigma.
Equations
- psigma.elim f a = a.cases_on f
@[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 (β (inhabited.default α))] :
Equations
- psigma.inhabited = {default := ⟨inhabited.default α _inst_1, inhabited.default (β (inhabited.default α)) _inst_2⟩}
@[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₂ (decidable.is_true _) = psigma.decidable_eq._match_2 a b₁ b₂ (h₂ a b₁ b₂)
- psigma.decidable_eq._match_1 a₁ _x a₂ _x_1 (decidable.is_false n) = decidable.is_false _
- psigma.decidable_eq._match_2 a b b (decidable.is_true _) = decidable.is_true _
- psigma.decidable_eq._match_2 a b₁ b₂ (decidable.is_false n) = decidable.is_false _
def
psigma.map
{α₁ : Sort u_3}
{α₂ : Sort u_4}
{β₁ : α₁ → Sort u_5}
{β₂ : α₂ → Sort u_6}
(f₁ : α₁ → α₂) :
Map the left and right components of a sigma
Equations
- psigma.map f₁ f₂ ⟨a, b⟩ = ⟨f₁ a, f₂ a b⟩