Some syntaх question

Stream: lean4

[YurySerdyuk]

Hi !
I would like to prove a property with some specific name P for a set S.
Formally , I would like to write something like this:

lemma name ( S : set type ) ( h : hypothesis about S ) : P S := by ...

But the Lean gives the message for such record :
function expected at
P
term has type
?m.62

What is wrong with my notation ?

[Ruben Van de Velde]

What does P mean?

[YurySerdyuk]

Some name

[Ruben Van de Velde]

Please share a #mwe, we can't help you with such vague questions

[YurySerdyuk]

More concretely I would like to prove that the specific collection of sets is a topology :

lemma openness (T : Set (Set ℤ)) (h : T = {O : Set ℤ | O = ∅ ∨ ∀ a ∈ O, ∃ b > 0, Set.range (fun n : ℤ => a + n * b) ⊆ O}) :
  IsTopology T := by
  rw [h]
  refine' ⟨by simp, _⟩

What is wrong with my syntax ?

[Ruben Van de Velde]

Missing imports, for a start

[YurySerdyuk]

import Mathlib.Data.Set.Basic

lemma openness (T : Set (Set ℤ)) (h : T = {O : Set ℤ | O = ∅ ∨ ∀ a ∈ O, ∃ b > 0, Set.range (fun n : ℤ => a + n * b) ⊆ O}) :
  IsTopology T := by
  rw [h]
  refine' ⟨by simp, _⟩
  -- Prove that the entire space ℤ is open.
  refine' ⟨by simp [Set.eq_univ_of_forall], _⟩

[Ruben Van de Velde]

Thanks. The issue is that IsTopology does not exist. Why did you think it would?

[Ruben Van de Velde]

That's a genuine question - how did you get to the point of writing IsTopology?

[YurySerdyuk]

I would like that isTopology would be the conjunction of the 4 corresponding properties. How to restructure the syntax of my proof ?

[Kevin Buzzard]

Is this code written by an LLM? Did you try reading a book on Lean?

[Ruben Van de Velde]

The first step if to define IsTopology, since it doesn't exist yet.

[Ruben Van de Velde]

But you still haven't answered my question why you wrote IsTopology in the first place