Theorems · Definition

Equiv.sigmaSigmaSubtype

{α : Type u_9} →
  {β : α → Type u_10} →
    {γ : (a : α) → β a → Type u_11} →
      (p : (a : α) × β a → Prop) →
        [uniq : Unique { ab // p ab }] → {a : α} → {b : β a} → p ⟨a, b⟩ → { s // p ⟨s.fst, s.snd.fst⟩ } ≃ γ a b

A subtype of a dependent triple which pins down both bases is equivalent to the respective fiber.

Defined in

Mathlib.Logic.Equiv.Basic

Cited by

3 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Unique