OAI/Combinatorics/InfiniteMatroid/Ideals.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.InfiniteMatroidCounterexample.SubsetIdeal line 12
2. lemma OAI.InfiniteMatroidCounterexample.SubsetIdeal.finite_sUnion line 22
3. lemma OAI.InfiniteMatroidCounterexample.SubsetIdeal.positive_nonempty line 30
4. lemma OAI.InfiniteMatroidCounterexample.SubsetIdeal.remove_small line 34
5. def OAI.InfiniteMatroidCounterexample.SubsetIdeal.ModSubset line 40
6. lemma OAI.InfiniteMatroidCounterexample.SubsetIdeal.modSubset_refl line 42
7. lemma OAI.InfiniteMatroidCounterexample.SubsetIdeal.modSubset_of_subset line 45
8. lemma OAI.InfiniteMatroidCounterexample.SubsetIdeal.modSubset_trans line 48
9. lemma OAI.InfiniteMatroidCounterexample.SubsetIdeal.modSubset_congr line 52
10. def OAI.InfiniteMatroidCounterexample.columnPattern line 64

    Source documentation

    A finite signed column pattern.

    def columnPattern {α ι : Type*} (G : ι → Set α) (F H : Finset ι) : Set α :=
    …

11. def OAI.InfiniteMatroidCounterexample.Forbidden line 67
12. lemma OAI.InfiniteMatroidCounterexample.forbidden_finite_avoidance line 70
13. lemma OAI.InfiniteMatroidCounterexample.exists_rank_ultrafilter line 109

    Source documentation

    The finite-intersection argument produces the required ultrafilter; no countable completeness or continuum regularity is used.

    lemma exists_rank_ultrafilter {α ι : Type*} (K : SubsetIdeal α) (G : ι → Set α)
        (hpattern : ∀ F H : Finset ι, Disjoint F H → ¬ K.small (columnPattern G F H)) :
        ∃ U : Ultrafilter α,
          (∀ N, K.small N → N ∉ U) ∧ (∀ t, G t ∈ U) ∧
          (∀ X, X ∈ U → {t | K.ModSubset X (G t)}.Finite) := by
    …

    Mentions: OAI.InfiniteMatroidCounterexample.SubsetIdeal, OAI.InfiniteMatroidCounterexample.columnPattern