Theorems · Theorem · combinatorics

Equiv.extendSubtype_mem

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

Defined in

Mathlib.Logic.Equiv.Fintype

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidablePredDecidablePredFinite