Theorems · Theorem · combinatorics

Equiv.extendSubtype.congr_simp

∀ {α : Type u_1} {p q : α → Prop} {inst : DecidablePred p} [inst_1 : DecidablePred p] {inst_2 : DecidablePred q}
  [inst_3 : DecidablePred q] [inst_4 : Finite ↑{x | p x}] (e e_1 : { x // p x } ≃ { x // q x }),
  e = e_1 → e.extendSubtype = e_1.extendSubtype

Defined in

Mathlib.Logic.Equiv.Fintype

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidablePredDecidablePredFinite