How to write arbitrary family of sets

Stream: lean4

[Santiago Mourenza Rivero]

I'm trying to prove the implication well order principle => choice axiom. The way I wanted to prove it is using the following definition of the choice axiom.

Having $\{X_i\}_{i\in I}$ a family of non-empty sets $\forall i \in I$, $\exist s : \{X_i\}_{i\in I} \to U i, X i$ satisfying $s (X_i) \in X_i , \forall i \in I$

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]
variable {β I : Type _}
variable {X : I → Set β}

open Set


def wop (S : Set α) (h₁ : S.Nonempty) (h₂ : ∀ s : Set α, s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, a ≤ b) : ∃ a ∈ S, ∀ b ∈ S, a ≤ b := by
  apply h₂
  apply h₁

--def ca (h₁ : ∀ (i : I), Nonempty (X i)) : ∃ s : ⋃ (i : I), X i, ∀ (i : I), s i ∈ (h₁ i).choose := by

def ca (h₁ : ∀ (i : I), Nonempty (X i)) : ∃ (s : (X i → ⋃ i, X i)), s (Classical.choice (h₁ i)) ∈ (X i) := by

The main problem is finding the syntax for creating this family and function s.

Thank you.

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

(deleted)

[loogle]

:exclamation: unknown identifier 'iUnion'
Did you mean "iUnion", Set.iUnion, or something else?

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

Oh sorry misread the question. Sincere apologies

[Shreyas Srinivas]

I suspect your definition is not computable since you classical choice.

[Eric Wieser]

Note you can use $$\Latex$$ ($\LaTeX$) in your post via double dollars; would you mind editing it?

[Shreyas Srinivas]

further you say you want to declare an axiom. The syntax for that is axiom <name> : <Proposition you want>

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

(deleted)

[Santiago Mourenza Rivero]

Shreyas Srinivas ha dicho:

The part that I am not able to understand is what you would like this to mean (X i → ⋃ i, X i)

Maybe is wrong but I wanted to make the function map from the family of set to the union of those sets

[Santiago Mourenza Rivero]

Eric Wieser ha dicho:

Note you can use $$\Latex$$ ($\LaTeX$) in your post via double dollars; would you mind editing it?

Thank you, I did it.

[Shreyas Srinivas]

I am stuck here :

axiom ca (h₁ : ∀ (i : I), Nonempty (X i)) : ∃ (s : ∀ i, (X i → ⋃ i, X i)), (s i (@Classical.choice (X i) (h₁ i))) ∈ X i := by

For the final part (s i (@Classical.choice (X i) (h₁ i))) ∈ X i, lean complains Membership (↑(⋃ i, X i)) (Set β) Here the coercion ↑(⋃ i, X i)) is @Elem β (⋃ i, X i) where Elem is supposed to mean Given the set s, Elem s is the Type of element of s

[Eric Wieser]

This works:

def ca (h₁ : ∀ (i : I), Nonempty (X i)) : ∃ (s : (X i → ⋃ i, X i)), (s (Classical.choice (h₁ i)) : β) ∈ X i :=
  ⟨fun x => ⟨x, subset_iUnion _ _ x.prop⟩, (Classical.choice (h₁ i)).prop⟩

[Eric Wieser]

Your statement looks fishy though; did you really mean to globally fix i (indeed, @Shreyas Srinivas' version does not)? I recommend adding set_option autoImplicit false and fixing the new error, because the automatic fix you're currently getting doesn't look like the one you actually want

[Shreyas Srinivas]

Oh. I forget that sometimes coercions have to be made explicit (although I don't understand why it didn't automatically get inferred here).

[Shreyas Srinivas]

In my case I got a syntax error at i when I turned the def into an axiom. So I was able to spot the mistake faster.

[Santiago Mourenza Rivero]

I was thinking about it and I tried to do this way but I think I am not understanding something about the types theory.

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]
variable {β I : Type _}
variable {X : I → Set β} --Toma un i ∈ I y le asigna un Xᵢ ∈ Set β
variable {i : I}
variable {S : Set α}

open Set


def wop (h₁ : S.Nonempty) (h₂ : ∀ s : Set α, s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, a ≤ b) : ∃ a ∈ S, ∀ b ∈ S, a ≤ b := by
  apply h₂
  apply h₁

theorem wop_implies_ca  (h₁ : S.Nonempty) (h₂ : ∀ s : Set α, s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, a ≤ b) (wop h₁ h₂) :
∃ (f : (Set β → Set β)), ∀ i : I, f (X i) ∈ (X i) := by
  sorry

[Santiago Mourenza Rivero]

I think I am not getting the point on how it works because I really don't understand the error I have. On the other hand I don't really get how the solutions you've sent works (maybe because of the syntaxis). Thank you for helping.

[Riccardo Brasca]

The error here is easy to understand: f has type Set β → Set β, so what does f (X i) ∈ (X i) mean?

[Riccardo Brasca]

X i is a term of type Set β, so its elements are terms of type β, but f (X i) is of type Set β, so it cannot be an element of X i

[Riccardo Brasca]

Note that I am not talking about paradoxes in set theory