about sInter

Stream: new members

[Ming Li]

import Mathlib.Order.FixedPoints
import Mathlib.Order.Zorn
set_option autoImplicit true
set_option warningAsError false

open Set Function
open Classical
universe u v
variable {α β : Type*}
variable (f : α → β)
variable (g : β → α)

def fcg : Set α → Set α
  | A => (g '' (f '' A)ᶜ)ᶜ
#check fcg f g

def  Omega: Set (Set α):= {A:Set α | (g '' (f '' A)ᶜ)ᶜ⊆ A}

#check Omega
#check ⋂₀ Omega f g

def setStar: Set α:=⋂₀ Omega f g

#check setStar f g
#check fcg setStar
example (f : α → β)(g : β → α): fcg '' setStar =setStar:=by

I am stucked here..have difficulty of coding math idea.

[Patrick Massot]

Please read #backticks and #mwe and edit your post accordingly. This will make it a lot easier to help you.

[Patrick Massot]

You should end with syntactically correct code such as

example (f : α → β)(g : β → α): fcg '' setStar = setStar:= by
  sorry

so that Lean gets a chance to give you an helpful error message.

[Patrick Massot]

What you wrote makes no sense at all, and I don't know what you intended to write.

[Patrick Massot]

Did you mean

example (f : α → β)(g : β → α): fcg f g (setStar f g) = setStar f g := by
  sorry

[Patrick Massot]

I have no idea what you are trying to express, I'm only crafting a meaningful statement that is syntactically close to what you wrote.

[Ming Li]

Thanks. That's what I mean. Are f(S) and f '' S the same?

[Kevin Buzzard]

On paper, yes. In Lean, f S makes no sense because f is expecting an element as an input.