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