WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Constructible universe

Revision #2794 → #3828 · back to history

modifiedDef operator6717111760c0
FieldFrom #2794To #3828
noteThe Def(X) operator (definable power set) is not present in Mathlib.The Def(X) operator (definable power set) is not present in Mathlib (the `ZFSet.Definable` class in SetTheory/ZFC/Basic is about definability of Lean set-functions, not first-order definable subsets).
addedV=L implies V_κ = L_κ for inaccessible κ106786fc0c09
addedIndiscernible-preserving maps extend to elementary self-embeddings of L1dfb94a1cfca