Theorems · Definition

Equiv.subtypeEquiv

{α : Sort u_1} →
  {β : Sort u_4} →
    {p : α → Prop} → {q : β → Prop} → (e : α ≃ β) → (∀ (a : α), p a ↔ q (e a)) → { a // p a } ≃ { b // q b }

If α is equivalent to β and the predicates p : α → Prop and q : β → Prop are equivalent at corresponding points, then {a // p a} is equivalent to {b // q b}. For the statement where α = β, that is, e : perm α, see Perm.subtypePerm.

Defined in

Mathlib.Logic.Equiv.Basic

Cited by

32 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound