Construction of maps

Stream: new members

[Suryansh Shrivastava]

So, I have constructed a partition on a particular type and created a map from this type to natural numbers such that all elements of a partition map to the same element. How can one lift this map, from sets of the partition to a natural number, i.e

import Mathlib.Data.Setoid.Partition
import Mathlib.Data.Real.Archimedean
noncomputable section

structure DeletedIntegerSpace where
  x : ℝ
  hn : x > 0
  hx : ∀ y : ℕ , x ≠ y

notation "ℝ+" => DeletedIntegerSpace

def modified_Ioo(b : ℕ) : Set ℝ+ :=
  {a : ℝ+ | a.1 ∈ Set.Ioo (b : ℝ) (b + 1 : ℝ )  }

def DIT_partition : Set (Set ℝ+) :=
  {S | ∃ (a : ℕ) , S = modified_Ioo a}

--I have proved this theorem already so don't worry about it
theorem DIT_partition_is_partition : Setoid.IsPartition DIT_partition  := by sorry

def f : ℝ+ → ℕ := λ x => Int.toNat ⌊x.x⌋
--I want to construct this map f' : Type: modified_Ioo → ℕ
--more  specifically  I have to prove the above function is injective

[Alex J. Best]

If you add import Mathlib.Data.Real.Archimedean your code should work (note that f must be a noncomputable def here also).
This imports both Mathlib.Data.Real.Basic which you need for ℝ to mean the reals, but also the definition of a docs#FloorRing, and the instance that says that the reals are such a structure, so that we can use the floor notation

[Notification Bot]

Suryansh Shrivastava has marked this topic as resolved.

[Notification Bot]

Suryansh Shrivastava has marked this topic as unresolved.

[Suryansh Shrivastava]

Alex J. Best said:

If you add import Mathlib.Data.Real.Archimedean your code should work (note that f must be a noncomputable def here also).
This imports both Mathlib.Data.Real.Basic which you need for ℝ to mean the reals, but also the definition of a docs#FloorRing, and the instance that says that the reals are such a structure, so that we can use the floor notation

Oh I didn't realise my code didn't work! I had just imported Mathlib in my original code so made a mistake while writing the #mwe

[Suryansh Shrivastava]

Should I look into first lifting the map to Setoid \R+ and the quotient the map?

[Alex J. Best]

I don't understand which map you are trying to construct sorry, can you explain some more

[Suryansh Shrivastava]

I want to construct the map f of type f : @Elem (Set ℝ+) DIT_partition → ℕ which is derived from my original map g : ℝ+ → ℕ := λ x => Int.toNat ⌊x.x⌋ and this map is well defined because all the elements of a partition map to the same element. My apologies, I made a wrong statement about this map being a lift

[Suryansh Shrivastava]

In my original project, I made a partition topology from the DIT_partition mentioned above and wanted to prove that DIT_Topology is
second countable space, and it requires me to get a function from DIT_Partition to Naturals and to prove the fact that it is injective.