Theorems · Theorem · combinatorics

Equiv.extendSubtype_apply_of_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 : α) (hx : p x), e.extendSubtype x = ↑(e ⟨x, hx⟩)

Defined in

Mathlib.Logic.Equiv.Fintype

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidablePredDecidablePredFinite