Diff — Naive set theory

Revision #1419 → #2460 · back to history

modifiedNaive set theory3d82b0f650ee

Field	From #1419	To #2460
mathlib.decl	—	—
mathlib.match_kind	—	—
mathlib.module	—	—
note	—	A meta-level historical/foundational label for informal set theories; not itself a Mathlib object (Mathlib.Data.Set.Defs provides the type-theoretic Set instead).
status	—	not_formalized

modifiedNaive theory (informal)89af48ecc7c0

Field	From #1419	To #2460
mathlib.decl	—	—
mathlib.match_kind	—	—
mathlib.module	—	—
note	—	A meta-mathematical description of non-formal theories, with no counterpart declaration in Mathlib.
status	—	not_formalized

modifiedRussell's paradoxbf0b33a9ddf6

Field	From #1419	To #2460
mathlib.decl	—	Class.univ_notMem_univ
mathlib.match_kind	—	special_case
mathlib.module	—	Mathlib.SetTheory.ZFC.Class
note	—	The paradox's conclusion that no universal set exists is captured in ZFC by Class.univ_notMem_univ (verified) and ZFSet.mem_irrefl, but the paradoxical set itself is not formally constructed.
status	—	partial

modifiedCantor's paradox derivationb96eb7971206

Field	From #1419	To #2460
mathlib.decl	—	Cardinal.cantor
mathlib.match_kind	—	special_case
mathlib.module	—	Mathlib.SetTheory.Cardinal.Order
note	—	Cantor's theorem a < 2^a underpinning the paradox is formalized as Cardinal.cantor (verified); the paradox as a naive-set derivation is not itself stated.
status	—	partial

modifiedGödel's incompleteness (consistency)8b9166f42252

Field	From #1419	To #2460
mathlib.decl	—	—
mathlib.match_kind	—	—
mathlib.module	—	—
note	—	Gödel's incompleteness theorems are not present in Mathlib; only unrelated first-order model-theory infrastructure (e.g., FirstOrder.Language.Theory.IsComplete) exists.
status	—	not_formalized

modifiedSet (Cantor)9ce8a08e9a3d

Field	From #1419	To #2460
mathlib.decl	—	Set
mathlib.match_kind	—	generalization
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	Sets over a type are `Set α := α → Prop` in Mathlib.Data.Set.Defs (verified).
status	—	formalized

modified4 is evene5579101ce77

Field	From #1419	To #2460
mathlib.decl	—	—
mathlib.match_kind	—	—
mathlib.module	—	—
note	—	A pedagogical example illustrating membership; not a stand-alone Mathlib fact (though Even 4 is trivially provable).
status	—	not_formalized

modifiedMembership78261a5a2294

Field	From #1419	To #2460
mathlib.decl	—	Set.Mem
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	Set membership is `Set.Mem` with the standard `Membership` instance in Mathlib.Data.Set.Defs (verified).
status	—	formalized

modifiedEquality of setsf40221559369

Field	From #1419	To #2460
mathlib.decl	—	Set.ext
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	Set.ext in Mathlib.Data.Set.Defs proves two sets equal iff they share the same members (verified).
status	—	formalized

modifiedPrimes less than 66301d7fa9921

Field	From #1419	To #2460
mathlib.decl	—	—
mathlib.match_kind	—	—
mathlib.module	—	—
note	—	A pedagogical example illustrating extensionality with no dedicated Mathlib lemma.
status	—	not_formalized

modifiedEmpty set7132304e044e

Field	From #1419	To #2460
mathlib.decl	—	Set.instEmptyCollection
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	The empty set on `Set α` is provided by the `EmptyCollection` instance (`∅ = fun _ ↦ False`) in Mathlib.Data.Set.Defs (read directly).
status	—	formalized

addedUniqueness of the empty setf69d0b7316b0

modifiedExtensional set notationb4534f2ba978

Field	From #1419	To #2460
mathlib.decl	—	Set.instSingletonSet
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	Roster notation `{a, b, ...}` is provided by the `Singleton` and `Insert` instances on `Set α` in Mathlib.Data.Set.Defs (read directly).
status	—	formalized

modifiedSet-builder notation6efe2670f6b4

Field	From #1419	To #2460
mathlib.decl	—	setOf
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	`{x \| p x}` desugars to `setOf p` with the elaborator defined in Mathlib.Data.Set.Defs (read directly).
status	—	formalized

modifiedSubset1c1707364a24

Field	From #1419	To #2460
mathlib.decl	—	Set.Subset
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	Set.Subset in Mathlib.Data.Set.Defs is defined as `∀ ⦃a⦄, a ∈ s₁ → a ∈ s₂` (read directly).
status	—	formalized

addedProper subset22eddc3d91ee

modifiedSupersetbdca51707ce3

Field	From #1419	To #2460
mathlib.decl	—	Set.instHasSubsetSet
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	`⊇` is the flip of `⊆` on `Set α`, available via the `HasSubset`/`LE` instances defined in Mathlib.Data.Set.Defs (read directly).
status	—	formalized

modifiedEquality via mutual inclusion4b78ddce6ed1

Field	From #1419	To #2460
mathlib.decl	—	Set.Subset.antisymm
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Basic
note	—	Set.Subset.antisymm gives A = B from A ⊆ B and B ⊆ A (verified via decl_exists).
status	—	formalized

modifiedEmpty set is subset of every setfcc1521cabbf

Field	From #1419	To #2460
mathlib.decl	—	Set.empty_subset
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Basic
note	—	Set.empty_subset proves `∅ ⊆ s` for any set (verified via decl_exists).
status	—	formalized

modifiedPower set6b91aad747d4

Field	From #1419	To #2460
mathlib.decl	—	Set.powerset
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	Set.powerset (`𝒫 s`) is `{t \| t ⊆ s}` in Mathlib.Data.Set.Defs (read directly).
status	—	formalized

addedCardinality of power set55084ddf6ce4

modifiedUniversal setffec1d33e8e4

Field	From #1419	To #2460
mathlib.decl	—	Set.univ
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	Set.univ := `{_a \| True}` is defined in Mathlib.Data.Set.Defs (read directly).
status	—	formalized

modifiedAbsolute complement0322a468434d

Field	From #1419	To #2460
mathlib.decl	—	Set.compl
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	Set.compl := `{a \| a ∉ s}` is defined in Mathlib.Data.Set.Defs (read directly).
status	—	formalized

modifiedUnion3ab6f4548b68

Field	From #1419	To #2460
mathlib.decl	—	Set.union
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	Set.union := `{a \| a ∈ s₁ ∨ a ∈ s₂}` is defined in Mathlib.Data.Set.Defs (read directly).
status	—	formalized

modifiedIntersection23f092becd9a

Field	From #1419	To #2460
mathlib.decl	—	Set.inter
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	Set.inter := `{a \| a ∈ s₁ ∧ a ∈ s₂}` is defined in Mathlib.Data.Set.Defs (read directly).
status	—	formalized

modifiedRelative complementf77b9d4711b4

Field	From #1419	To #2460
mathlib.decl	—	Set.diff
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Defs
note	—	Set.diff := `{a ∈ s \| a ∉ t}` (i.e. `s \ t`) is defined in Mathlib.Data.Set.Defs (read directly).
status	—	formalized

modifiedLeft-handed and blond people4b59cd58e655

Field	From #1419	To #2460
mathlib.decl	—	—
mathlib.match_kind	—	—
mathlib.module	—	—
note	—	Pedagogical illustration of union/intersection with no formal counterpart.
status	—	not_formalized

modifiedNo human over 1000 years3512088c3be3

Field	From #1419	To #2460
mathlib.decl	—	—
mathlib.match_kind	—	—
mathlib.module	—	—
note	—	Pedagogical illustration with no Mathlib analogue.
status	—	not_formalized

modifiedPower set Boolean algebraaa78c9bafbbd

Field	From #1419	To #2460
mathlib.decl	—	Set.instBooleanAlgebra
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Order.SetNotation
note	—	`Set α` carries a `BooleanAlgebra` instance under ∪, ∩, and complement in Mathlib's set order/lattice API.
status	—	formalized

modifiedOrdered pairf6beeca14177

Field	From #1419	To #2460
mathlib.decl	—	Prod
mathlib.match_kind	—	exact
mathlib.module	—	Init.Prelude
note	—	Ordered pairs are `Prod α β` from Init.Prelude (verified via decl_exists).
status	—	formalized

modifiedEquality of ordered pairs51896d79a19e

Field	From #1419	To #2460
mathlib.decl	—	Prod.mk.injEq
mathlib.match_kind	—	exact
mathlib.module	—	Init.Core
note	—	Prod.mk.injEq: `((a,b) = (c,d)) = (a = c ∧ b = d)` (verified via loogle).
status	—	formalized

modifiedCartesian product19ad1317c001

Field	From #1419	To #2460
mathlib.decl	—	Set.prod
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Set.Operations
note	—	Set.prod builds `s ×ˢ t = {p \| p.1 ∈ s ∧ p.2 ∈ t}` in Mathlib.Data.Set.Operations (verified via decl_exists).
status	—	formalized

modifiedNatural numbersafcbb297eda7

Field	From #1419	To #2460
mathlib.decl	—	Nat
mathlib.match_kind	—	exact
mathlib.module	—	Init.Prelude
note	—	Nat is the core natural-number type (verified via decl_exists).
status	—	formalized

modifiedIntegersec654ab3fbcb

Field	From #1419	To #2460
mathlib.decl	—	Int
mathlib.match_kind	—	exact
mathlib.module	—	Init.Data.Int.Basic
note	—	Int is the core integer inductive type (verified via decl_exists).
status	—	formalized

modifiedRational numberscd1aec381bdf

Field	From #1419	To #2460
mathlib.decl	—	Rat
mathlib.match_kind	—	exact
mathlib.module	—	Init.Data.Rat.Basic
note	—	Rat is the core rationals type (verified via decl_exists).
status	—	formalized

modifiedAlgebraic numbersb12532a3fd0d

Field	From #1419	To #2460
mathlib.decl	—	AlgebraicClosure
mathlib.match_kind	—	generalization
mathlib.module	—	Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
note	—	Mathlib formalizes `IsAlgebraic` and `AlgebraicClosure ℚ`, but there is no distinguished type `𝔸` of algebraic numbers as a named subfield of ℂ (verified via decl_exists).
status	—	partial

modifiedReal numbersd6cc5cb09dc7

Field	From #1419	To #2460
mathlib.decl	—	Real
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Real.Basic
note	—	Real is Mathlib's Cauchy-completion of ℚ (verified via decl_exists).
status	—	formalized

modifiedComplex numberscb2e8c14bb4d

Field	From #1419	To #2460
mathlib.decl	—	Complex
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.Data.Complex.Basic
note	—	Complex is Mathlib's field of complex numbers (verified via decl_exists).
status	—	formalized

addedAxiom schema of unrestricted comprehension32fdba0082a4

addedAxiom schema of specificationfd291142cf95

modifiedBurali-Forti paradox6cdf8b808e4a

Field	From #1419	To #2460
mathlib.decl	—	ZFSet.isOrdinal_notMem_univ
mathlib.match_kind	—	special_case
mathlib.module	—	Mathlib.SetTheory.ZFC.Class
note	—	The conclusion of Burali–Forti — that the ordinals form a proper class — is captured by ZFSet.isOrdinal_notMem_univ (verified); the paradox itself is not named.
status	—	partial

modifiedCantor's paradoxd06a9064eb06

Field	From #1419	To #2460
mathlib.decl	—	Cardinal.cantor
mathlib.match_kind	—	special_case
mathlib.module	—	Mathlib.SetTheory.Cardinal.Order
note	—	Cantor's theorem `a < 2^a` behind the paradox is Cardinal.cantor (verified); the naive-set paradox itself is not stated.
status	—	partial

modifiedRussell's paradox (formula)0118f98ffe87

Field	From #1419	To #2460
mathlib.decl	—	Class.univ_notMem_univ
mathlib.match_kind	—	special_case
mathlib.module	—	Mathlib.SetTheory.ZFC.Class
note	—	The Russell class of non-self-membered sets isn't constructed, but `Class.univ_notMem_univ` and `ZFSet.mem_irrefl` (verified) show the paradoxical set cannot exist.
status	—	partial

modifiedNo universef1adc581fe99

Field	From #1419	To #2460
mathlib.decl	—	Class.univ_notMem_univ
mathlib.match_kind	—	special_case
mathlib.module	—	Mathlib.SetTheory.ZFC.Class
note	—	That the universal class is not itself a set is formalized as Class.univ_notMem_univ (verified via decl_exists).
status	—	partial

modifiedCurry's paradox80460b8995aa

Field	From #1419	To #2460
mathlib.decl	—	—
mathlib.match_kind	—	—
mathlib.module	—	—
note	—	Curry's paradox has no counterpart declaration in Mathlib.
status	—	not_formalized

addedAxiom of regularity529c012fa5f5

modifiedNo set is element of itselfafeec20c1173

Field	From #1419	To #2460
mathlib.decl	—	ZFSet.mem_irrefl
mathlib.match_kind	—	exact
mathlib.module	—	Mathlib.SetTheory.ZFC.Basic
note	—	ZFSet.mem_irrefl: `∀ (x : ZFSet), x ∉ x` (verified via decl_exists).
status	—	formalized