how to apply intermediate_value_Icc here

Stream: new members

[Jame GA]

Hello, I come across a problem recently when applying intermediate, infoview says that typeclass instance problem is stuck. It must be something about the typeclass of I, I guess, but I have no experience dealing with such things, any advice for me? Thanks in advance!

  lemma obtain_fix_pt (J : Set ℝ) (I : Set J) {G : J → ℝ} (cI : is_interval I)(hG : Continuous G)(h : (I : Set ℝ ) ⊂ G '' I) : ∃ (p : I), G p = p :=by
  have end_ab : ∃ (a : ℝ) (b : ℝ)(aleb : a ≤ b), I = Set.Icc a b :=by
    apply cI
  rcases end_ab with ⟨a, b, aleb, hab⟩
  have e₁: ∃ a₁ : I , G a₁= a ∧ (a₁ - G a₁ ≥ 0) :=by sorry
  have e₂ :∃ b₂ : I , G b₂= b ∧ (b₂ - G b₂ ≤ 0) :=by sorry

  rcases e₁ with ⟨a₁, pa₁⟩
  rcases e₂ with ⟨b₂, pb₂⟩
  let f := λ x : I  ↦ (x - G (x : J))
  have hf: ContinuousOn f (Set.Icc a₁ b₂) :=by sorry

  have := intermediate_value_Icc aleb hf

[Luigi Massacci]

You may want to post a #mwe. What is is_interval?

[Gareth Ma]

Can you share your definition of is_interval?

[Luigi Massacci]

Gareth Ma said:

Can you share your definition of is_interval?

Beat me to it...

[Gareth Ma]

Screenshot-2024-03-05-at-15.44.43.png

You beat me to it, no?

[Gareth Ma]

race conditions :rolling_eyes:

[Jame GA]

Luigi Massacci 发言道：

You may want to post a #mwe. What is is_interval?

oh, my fault! It is just a restatement of Set.Icc for convenience

def is_interval (J : Set ℝ) : Prop := ∃ (a : ℝ) (b : ℝ)(aleb : a ≤ b), J = Set.Icc a b

[Jame GA]

forgive me, I was offline yesterday