Theorems · Theorem

Equiv.subtypeEquiv_apply

∀ {α : Sort u_1} {β : Sort u_4} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a))
  (a : { a // p a }), (e.subtypeEquiv h) a = ⟨e ↑a, ⋯⟩

Defined in

Mathlib.Logic.Equiv.Basic

Cited by

8 results in Mathlib

Foundations

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