## Stream: maths

### Topic: generate filter

#### Kenny Lau (Apr 28 2018 at 04:50):

def generate {α : Type u} (s :set (set α)) : filter α :=
{ sets := { A | ∃ t ⊆ s, ⋂₀ t ⊆ A },
univ := ⟨∅, set.empty_subset s, @set.sInter_empty α ▸ set.subset.refl _⟩,
up   := λ x ⟨t, ht1, ht2⟩ y H2, ⟨t, ht1, set.subset.trans ht2 H2⟩,
down := λ x ⟨t, ht1, ht2⟩ y ⟨u, hu1, hu2⟩, ⟨x ∩ y,
⟨t ∪ u, set.union_subset ht1 hu1, (set.sInter_union t u).symm ▸
set.subset_inter
(set.subset.trans (set.inter_subset_left _ _) ht2)
(set.subset.trans (set.inter_subset_right _ _) hu2)⟩,
set.inter_subset_left _ _, set.inter_subset_right _ _⟩ }


#### Kenny Lau (Apr 28 2018 at 04:50):

in mathlib it's done by taking the infimum of the principal filters lol

#### Kenny Lau (Apr 28 2018 at 04:55):

aha, that's the wrong definition

#### Reid Barton (Apr 28 2018 at 04:56):

Those mathlib-style definitions are actually quite convenient because you can immediately use them with lemmas like vmap_infi, vmap_principal, etc.

#### Kenny Lau (Apr 28 2018 at 05:17):

/-- The filter generated by a set of sets. -/
def generate (s :set (set α)) : filter α :=
{ sets  := { A | ∃ t ⊆ s, set.finite t ∧ ⋂₀ t ⊆ A },
univ  := ⟨∅, set.empty_subset s, set.finite_empty, @set.sInter_empty α ▸ set.subset.refl _⟩,
up    := λ x ⟨t, ht1, ht2, ht3⟩ y H2, ⟨t, ht1, ht2, set.subset.trans ht3 H2⟩,
inter := λ x ⟨t, ht1, ht2, ht3⟩ y ⟨u, hu1, hu2, hu3⟩,
⟨t ∪ u, set.union_subset ht1 hu1, set.finite_union ht2 hu2,
(set.sInter_union t u).symm ▸ set.subset_inter
(set.subset.trans (set.inter_subset_left _ _) ht3)
(set.subset.trans (set.inter_subset_right _ _) hu3)⟩ }

/-- The filter generated contains the original sets. -/
theorem generate.subset (s :set (set α)) : s ⊆ (generate s).sets :=
λ A HA, ⟨{A}, set.singleton_subset_iff.2 HA, set.finite_singleton A,
(set.sInter_singleton A).symm ▸ set.subset.refl A⟩

/-- The filter generated is the smallest filter containing the original sets. -/
theorem generate.min (s :set (set α)) {f : filter α} (H : s ⊆ f.sets) :
(generate s).sets ⊆ f.sets :=
λ A ⟨t, ht1, ht2, ht3⟩, (set.finite.induction_on ht2
(λ A _ HA, have H1 : A = set.univ,
from set.eq_univ_of_univ_subset $@set.sInter_empty α ▸ HA, H1.symm ▸ f.univ) (λ B t _ _ ih A ht1 ht3, f.up (⋂₀ insert B t) ((set.sInter_insert B t).symm ▸ f.inter B (H$ ht1 \$ set.mem_insert _ _)
(⋂₀ t) (ih _ (set.insert_subset.1 ht1).2 (set.subset.refl _))) _ ht3)) A ht1 ht3

/-- The filter generated by one element. -/
def principal {α : Type u} (s : set α) : filter α :=
generate {s}


#### Kenny Lau (Apr 28 2018 at 05:18):

that's the right definition

#### Kenny Lau (Apr 28 2018 at 05:18):

and I learnt how to use set.finite.induction_on :P

#### Kenny Lau (Apr 28 2018 at 05:19):

@Kevin Buzzard do you think that's enough interface?

Last updated: May 09 2021 at 09:11 UTC