From 98e83c3d541c77cdb7da20d79611a780ff8e7d90 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Tue, 7 Feb 2023 20:26:31 +0000
Subject: [PATCH] feat(set_theory/zfc/basic): define `hereditarily` (#18328)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

We will define von Neumann ordinals as hereditarily transitive sets in #18329. Also there are [hereditarily finite sets](https://en.wikipedia.org/wiki/Hereditarily_finite_set) and [hereditarily countable sets](https://en.wikipedia.org/wiki/Hereditarily_countable_set) in set theory.

Co-authored-by: Violeta Hernández [vi.hdz.p@gmail.com](mailto:vi.hdz.p@gmail.com)
---
 src/set_theory/zfc/basic.lean | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/src/set_theory/zfc/basic.lean b/src/set_theory/zfc/basic.lean
index d5b8d9422ab14..7396b9188f529 100644
--- a/src/set_theory/zfc/basic.lean
+++ b/src/set_theory/zfc/basic.lean
@@ -44,6 +44,8 @@ Then the rest is usual set theory.
   function `x → y`. That is, each member of `x` is related by the ZFC set to exactly one member of
   `y`.
 * `Set.funs`: ZFC set of ZFC functions `x → y`.
+* `Set.hereditarily p x`: Predicate that every set in the transitive closure of `x` has property
+  `p`.
 * `Class.iota`: Definite description operator.
 
 ## Notes
@@ -857,6 +859,36 @@ theorem map_unique {f : Set.{u} → Set.{u}} [H : definable 1 f] {x z : Set.{u}}
 λ h, ⟨λ y yx, let ⟨z, zx, ze⟩ := mem_image.1 yx in ze ▸ pair_mem_prod.2 ⟨zx, h z zx⟩,
      λ z, map_unique⟩⟩
 
+/-- Given a predicate `p` on ZFC sets. `hereditarily p x` means that `x` has property `p` and the
+members of `x` are all `hereditarily p`. -/
+def hereditarily (p : Set → Prop) : Set → Prop
+| x := p x ∧ ∀ y ∈ x, hereditarily y
+using_well_founded { dec_tac := `[assumption] }
+
+section hereditarily
+
+variables {p : Set.{u} → Prop} {x y : Set.{u}}
+
+lemma hereditarily_iff :
+  hereditarily p x ↔ p x ∧ ∀ y ∈ x, hereditarily p y :=
+by rw [← hereditarily]
+
+alias hereditarily_iff ↔ hereditarily.def _
+
+lemma hereditarily.self (h : x.hereditarily p) : p x := h.def.1
+lemma hereditarily.mem (h : x.hereditarily p) (hy : y ∈ x) : y.hereditarily p := h.def.2 _ hy
+
+lemma hereditarily.empty : hereditarily p x → p ∅ :=
+begin
+  apply x.induction_on,
+  intros y IH h,
+  rcases Set.eq_empty_or_nonempty y with (rfl|⟨a, ha⟩),
+  { exact h.self },
+  { exact IH a ha (h.mem ha) }
+end
+
+end hereditarily
+
 end Set
 
 /-- The collection of all classes.