Theorems · Theorem · logic and foundations
Equiv.setCongr_apply
∀ {α : Type u_3} {s t : Set α} (h : s = t) (a : { a // (fun x => x ∈ s) a }), (Equiv.setCongr h) a = ⟨↑a, ⋯⟩- Defined in
- Mathlib.Logic.Equiv.Set
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement and proof · cited by 53,352
- Equivstatement · cited by 8,337
- Set.Elemstatement · cited by 7,166
- Equiv.reflstatement · cited by 274
- Equiv.setCongrstatement and proof · cited by 13
Cited by5
Results whose statement or proof uses this declaration.
- Set.coe_snd_biUnionEqSigmaOfDisjointproof · cited by 1
- Profinite.NobelingProof.Products.evalFacPropsproof · cited by 1
- algebraicIndependent_of_set_of_finiteproof · cited by 1
- Equiv.Perm.Disjoint.isConj_mulproof · cited by 1
- Sion.exists_lt_iInf_of_lt_iInf_of_supproof · cited by 1