Theorems · Theorem

Equiv.Perm.subtypeCongr.left_apply

∀ {ε : Type u_9} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a })
  {a : ε} (h : p a), (ep.subtypeCongr en) a = ↑(ep ⟨a, h⟩)

Defined in

Mathlib.Logic.Equiv.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidablePred