Zulip Chat Archive

Stream: general

Topic: How to use Equiv.Set.univ


Santiago Mourenza Rivero (Jun 17 2024 at 08:49):

I'm trying to finish a result where I need to use that the set m.s = univ, the problem is that the types don't unify as I expected and I wanted to use this equivalence but I am not sure how to do it. The last line (where I comment what I am looking for) is where I'm working:

import Mathlib.Tactic
import Mathlib.Init.Order.Defs

variable (γ : Type _)

variable {I : Type _}
variable (X : I  Set γ)
variable (S : Set γ )

open Set
open Classical

def is_chain [PartialOrder γ] (c : Set γ) : Prop :=  (x y : γ), x  c  y  c  x  y  y  x

def is_well_ordered (R : γ   γ  Prop) : Prop :=  (A : Set γ), Nonempty A   n  A,  m  A, R n m
def well_ordered_principle : Prop :=  (R : γ   γ  Prop), is_well_ordered γ R

variable {γ}

def inductive_set [PartialOrder γ] (S : Set γ) : Prop :=  (c : Set γ), c  S  is_chain γ c   (ub : γ),  (x : γ ), x  c  x  ub
def zorn [PartialOrder γ] (_ : inductive_set S ) : Prop :=  (m : γ), m  S   (x : γ), x  S  x < m

@[ext]structure WellOrderedSet (γ : Type _) :=
(s : Set γ)
(r : γ   γ   Prop)
(h_well : is_well_ordered s (fun x y => r x.val y.val))
(h_triv :  (x y : γ) (_ : x  s  y  s), ¬ r x y)

variable (F : Set (WellOrderedSet γ))

instance : PartialOrder (WellOrderedSet γ) where
  le := sorry
  lt := sorry
  le_refl := sorry
  le_trans := sorry
  lt_iff_le_not_le := sorry
  le_antisymm := sorry

lemma F_is_inductive : inductive_set F := by sorry

theorem zorn_implies_wop : zorn F (F_is_inductive F)  well_ordered_principle γ := by
  intro hZ
  rw[zorn] at hZ
  rw[well_ordered_principle]
  obtain m, hm := hZ
  have : m.s = Set.univ := sorry
  use m.r
  have h3 := m.3
  --Here is where I need to use Equiv.Set.univ and using h3 I can finish the result
  sorry

Last updated: May 02 2025 at 03:31 UTC