From ff2c9d6d2d2cdccc9bf94b4f246b44aa71e6e338 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Thu, 2 Jan 2025 11:03:42 +0000 Subject: [PATCH] feat(BooleanSubalgebra): closure of supClosed+infClosed set containing bot+top (#20251) Every element in the closure of such a set `s` can be written as a finite sup of elements of the form `a \ b` with `a`, `b` in `s`. --- Mathlib/Order/BooleanSubalgebra.lean | 38 ++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/Mathlib/Order/BooleanSubalgebra.lean b/Mathlib/Order/BooleanSubalgebra.lean index ca4126280f883..24751706b1099 100644 --- a/Mathlib/Order/BooleanSubalgebra.lean +++ b/Mathlib/Order/BooleanSubalgebra.lean @@ -361,6 +361,44 @@ lemma closure_bot_sup_induction {p : ∀ g ∈ closure s, Prop} (mem : ∀ x hx, compl_mem' := fun ⟨_, hb⟩ ↦ ⟨_, compl _ _ hb⟩ } closure_le (L := L).mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id +section sdiff_sup + +variable (sup : SupClosed s) (inf : InfClosed s) (bot_mem : ⊥ ∈ s) (top_mem : ⊤ ∈ s) +include sup inf bot_mem top_mem + +theorem mem_closure_iff_sup_sdiff {a : α} : + a ∈ closure s ↔ ∃ t : Finset (s × s), a = t.sup fun x ↦ x.1.1 \ x.2.1 := by + classical + refine ⟨closure_bot_sup_induction + (fun x h ↦ ⟨{(⟨x, h⟩, ⟨⊥, bot_mem⟩)}, by simp⟩) ⟨∅, by simp⟩ ?_ ?_, ?_⟩ + · rintro ⟨t, rfl⟩ + exact t.sup_mem _ (subset_closure bot_mem) (fun _ h _ ↦ sup_mem h) _ + fun x hx ↦ sdiff_mem (subset_closure x.1.2) (subset_closure x.2.2) + · rintro _ - _ - ⟨t₁, rfl⟩ ⟨t₂, rfl⟩ + exact ⟨t₁ ∪ t₂, by rw [Finset.sup_union]⟩ + rintro x - ⟨t, rfl⟩ + refine t.induction ⟨{(⟨⊤, top_mem⟩, ⟨⊥, bot_mem⟩)}, by simp⟩ fun ⟨x, y⟩ t _ ⟨tc, eq⟩ ↦ ?_ + simp_rw [Finset.sup_insert, compl_sup, eq] + refine tc.induction ⟨∅, by simp⟩ fun ⟨z, w⟩ tc _ ⟨t, eq⟩ ↦ ?_ + simp_rw [Finset.sup_insert, inf_sup_left, eq] + refine ⟨{(z, ⟨_, sup x.2 w.2⟩), (⟨_, inf y.2 z.2⟩, w)} ∪ t, ?_⟩ + simp_rw [Finset.sup_union, Finset.sup_insert, Finset.sup_singleton, sdiff_eq, + compl_sup, inf_left_comm z.1, compl_inf, compl_compl, inf_sup_right, inf_assoc] + +@[elab_as_elim] theorem closure_sdiff_sup_induction {p : ∀ g ∈ closure s, Prop} + (sdiff : ∀ x hx y hy, p (x \ y) (sdiff_mem (subset_closure hx) (subset_closure hy))) + (sup' : ∀ x hx y hy, p x hx → p y hy → p (x ⊔ y) (sup_mem hx hy)) + {x} (hx : x ∈ closure s) : p x hx := by + obtain ⟨t, rfl⟩ := (mem_closure_iff_sup_sdiff sup inf bot_mem top_mem).mp hx + revert hx + classical + refine t.induction (by simpa using sdiff _ bot_mem _ bot_mem) fun x t _ ih hxt ↦ ?_ + simp only [Finset.sup_insert] at hxt ⊢ + exact sup' _ _ _ _ (sdiff _ x.1.2 _ x.2.2) + (ih <| (mem_closure_iff_sup_sdiff sup inf bot_mem top_mem).mpr ⟨_, rfl⟩) + +end sdiff_sup + end BooleanAlgebra section CompleteBooleanAlgebra