ascending/decending lemmata related `Set` and `Finset`

Stream: Is there code for X?

[SnO2WMaN]

I believe both of the following statements are correct, and might be already similar or exact results exists in Mathlib4, but I'm now sure where. It'd be helpful If you could let me know.

finset_enumerate asserts that any infinite set can be infinitely approximated by ascending family of finite sets starts with {x}.

no_infinite_ssubset_chain states that no infinite descending ⊂-chain exists on Finset.

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finite.Defs

variable {α}

lemma split_finset {X : Set α} (X_infinite : X.Infinite) {a : α} : ∃ f : ℕ → Finset α, ((f 0) = {a}) ∧ (∀ i, f i ⊂ f (i + 1)) ∧ (∀ i, ↑(f i) ⊆ X) ∧ (∀ b ∈ X, ∃ i, b ∈ f i) := by sorry

lemma no_infinite_ssubset_chain {f : ℕ → Finset α} : ¬(∀ i, ∃ j > i, f j ⊂ f i) := by sorry

[Aaron Liu]

split_finset is false (only true for countable sets containing a)

[Aaron Liu]

no_infinite_ssubset_chain is also false and does not say what you say it says

[SnO2WMaN]

ah sorry no_infinite_ssubset_chain is forgot to write negation.

[Violeta Hernández]

Presumably you're looking for a WellFoundedLT (Finset α) instance?

[Aaron Liu]

no it's the WellFoundedLT

[Violeta Hernández]

docs#Finset.wellFoundedLT

[SnO2WMaN]

Thanks!

[Violeta Hernández]

Combine this with docs#wellFounded_iff_isEmpty_descending_chain

[Aaron Liu]

Mashu Noguchi said:

ah sorry no_infinite_ssubset_chain is forgot to write negation.

Your corrected version is true now and you can prove it with the lemmas Violeta Hernández is showing you

[SnO2WMaN]

no_infinite_ssubset_chain looks proved by this way. split_finset might be proved: i forgot to write a ∈ X and α is actually ℕ. I apologize for overgeneralizing when extracting these lemmata from where actually i needed.

[Aaron Liu]

Mashu Noguchi said:

no_infinite_ssubset_chain looks proved by this way. split_finset might be proved: i forgot to write a ∈ X and α is actually ℕ. I apologize for overgeneralizing when extracting these lemmata from where actually i needed.

Here's a version I can prove

import Mathlib

example {α : Type*} {X : Set α} (count : X.Countable) (inf : X.Infinite) {a : α} (ha : a ∈ X) :
    ∃ f : ℕ → Finset α, ((f 0) = {a}) ∧ (∀ i, f i ⊂ f (i + 1)) ∧
      (∀ i, ↑(f i) ⊆ X) ∧ (∀ b ∈ X, ∃ i, b ∈ f i) := by
  let X' := X \ {a}
  have count' : Countable X' := (count.mono Set.diff_subset).to_subtype
  have inf' : Infinite X' := (inf.diff (Set.finite_singleton a)).to_subtype
  obtain ⟨eq⟩ : Nonempty (Nat ≃ X') := nonempty_equiv_of_countable
  refine ⟨fun n => Finset.cons a ((Finset.range n).map
    (eq.toEmbedding.trans (Function.Embedding.subtype _))) ?_, ?_, ?_, ?_, ?_⟩
  · -- simp?
    simp only [Finset.mem_map, Finset.mem_range, Function.Embedding.trans_apply,
      Equiv.coe_toEmbedding, Function.Embedding.subtype_apply, not_exists, not_and]
    intro x _
    exact (eq x).prop.right
  · rfl
  · simp [Finset.ssubset_def]
  · intro i
    -- simp? [Set.insert_subset_iff, ha]
    simp only [Finset.coe_cons, Finset.coe_map, Function.Embedding.trans_apply,
      Equiv.coe_toEmbedding, Function.Embedding.subtype_apply, Finset.coe_range,
      Set.insert_subset_iff, ha, Set.image_subset_iff, true_and]
    intro x _
    exact (eq x).prop.left
  · intro b hb
    by_cases hba : b = a
    · exact ⟨0, by simp [hba]⟩
    · refine ⟨eq.symm ⟨b, hb, hba⟩ + 1, ?_⟩
      apply Finset.mem_cons_of_mem
      -- simp?
      simp only [Finset.mem_map, Finset.mem_range, Function.Embedding.trans_apply,
        Equiv.coe_toEmbedding, Function.Embedding.subtype_apply]
      exact ⟨eq.symm ⟨b, hb, hba⟩, by simp⟩

[SnO2WMaN]

Violeta Hernández said:

Combine this with docs#wellFounded_iff_isEmpty_descending_chain

¬(∀ i, f (i + 1) ⊂ f i)is clearly proved showed way. and I thought ¬(∀ i, ∃ j > i, f j ⊂ f i)is obvious too, but I can't do, is it really true?

[Aaron Liu]

docs#strictMono_nat_of_lt_succ

[Aaron Liu]

probably

[Aaron Liu]

no we want the dual docs#strictAnti_nat_of_succ_lt

[SnO2WMaN]

yes, exactly we want to (∀ (i : ℕ), ∃ j > i, f j ⊂ f i) → (∀ (i : ℕ), f (i + 1) ⊂ f i).

case zero is obvious, but succ case is how...?

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finite.Defs
import Mathlib.Order.WellFounded

lemma Finset.no_ssubset_descending_chain'  {f : ℕ → Finset α} : ¬(∀ i, f (i + 1) ⊂ f i) := by
  by_contra hC;
  apply wellFounded_iff_isEmpty_descending_chain.mp Finset.wellFoundedLT.wf |>.false;
  exact ⟨f, hC⟩;

lemma Finset.no_ssubset_descending_chain  {f : ℕ → Finset α} : ¬(∀ i, ∃ j > i, f j ⊂ f i) := by
  have := Finset.no_ssubset_descending_chain' (f := f);
  contrapose! this;
  intro i;
  obtain ⟨j, _, hfjfi⟩ := this i;
  obtain ⟨k, rfl⟩ : ∃ k, j = (i + 1) + k := by use (j - i - 1); omega;
  induction k with
  | zero => simpa;
  | succ k ih =>
    sorry;

[Aaron Liu]

import Mathlib.Data.Finset.Defs

lemma Finset.no_ssubset_descending_chain  {f : ℕ → Finset α} : ¬(∀ i, ∃ j > i, f j ⊂ f i) := by
  intro h
  have n := 0
  induction hf : f n using WellFoundedLT.fix generalizing n with subst hf | _ _ ih
  obtain ⟨m, -, hy⟩ := h n
  exact ih (f m) hy m rfl

[Aaron Liu]

no need to make it complicated

[Aaron Liu]

I think I used almost all the features of induction in one line

[SnO2WMaN]

Greateful Thanks @Aaron Liu , I proved my tasks.

https://github.com/FormalizedFormalLogic/Foundation/pull/533/files#diff-3b17de73fdb9217d65755401bb557c6fc5e9690787f5af338393bf5f75218892R15-R63