Membership in intervals via Int.floor / Nat.floor / Int.ceil / Nat.ceil

For a FloorRing (resp. FloorSemiring) α, we relate membership of a cast ↑n in an interval of α to membership of the integer (resp. natural number) n in the corresponding interval with floor/ceil endpoints, for instance Int.cast_mem_Ioc_iff : ↑n ∈ Set.Ioc a b ↔ n ∈ Set.Ioc ⌊a⌋ ⌊b⌋. If the right-hand side set is finite, we express it as Finset instead.

In the natural number case, non-negativity hypotheses are required when the Nat.floor function is involved. In the IsStrictOrderedRing case, one of these hypotheses can be omitted.

theorem Int.cast_mem_Ioc_iff {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {a b : α} {n : ℤ} : ↑n ∈ Set.Ioc a b ↔ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋

theorem Int.cast_mem_Ico_iff {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {a b : α} {n : ℤ} : ↑n ∈ Set.Ico a b ↔ n ∈ Finset.Ico ⌈a⌉ ⌈b⌉

theorem Int.cast_mem_Icc_iff {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {a b : α} {n : ℤ} : ↑n ∈ Set.Icc a b ↔ n ∈ Finset.Icc ⌈a⌉ ⌊b⌋

theorem Int.cast_mem_Ioo_iff {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {a b : α} {n : ℤ} : ↑n ∈ Set.Ioo a b ↔ n ∈ Finset.Ioo ⌊a⌋ ⌈b⌉

theorem Int.cast_mem_Ioi_iff {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {a : α} {n : ℤ} : ↑n ∈ Set.Ioi a ↔ n ∈ Set.Ioi ⌊a⌋

theorem Int.cast_mem_Ici_iff {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {a : α} {n : ℤ} : ↑n ∈ Set.Ici a ↔ n ∈ Set.Ici ⌈a⌉

theorem Int.cast_mem_Iic_iff {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {b : α} {n : ℤ} : ↑n ∈ Set.Iic b ↔ n ∈ Set.Iic ⌊b⌋

theorem Int.cast_mem_Iio_iff {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {b : α} {n : ℤ} : ↑n ∈ Set.Iio b ↔ n ∈ Set.Iio ⌈b⌉

theorem Nat.cast_mem_Ioc_iff {α : Type u_1} [Semiring α] [LinearOrder α] [FloorSemiring α] {a b : α} {n : ℕ} (ha : 0 ≤ a) (hb : 0 ≤ b) : ↑n ∈ Set.Ioc a b ↔ n ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊

theorem Nat.cast_mem_Ioc_iff' {α : Type u_1} [Semiring α] [LinearOrder α] [FloorSemiring α] {a b : α} {n : ℕ} [IsStrictOrderedRing α] (ha : 0 ≤ a) : ↑n ∈ Set.Ioc a b ↔ n ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊

The 0 ≤ b hypothesis in cast_mem_Ioc_iff can be dropped if IsStrictOrderedRing α.

theorem Nat.cast_mem_Ico_iff {α : Type u_1} [Semiring α] [LinearOrder α] [FloorSemiring α] {a b : α} {n : ℕ} : ↑n ∈ Set.Ico a b ↔ n ∈ Finset.Ico ⌈a⌉₊ ⌈b⌉₊

theorem Nat.cast_mem_Icc_iff {α : Type u_1} [Semiring α] [LinearOrder α] [FloorSemiring α] {a b : α} {n : ℕ} (hb : 0 ≤ b) : ↑n ∈ Set.Icc a b ↔ n ∈ Finset.Icc ⌈a⌉₊ ⌊b⌋₊

theorem Nat.cast_mem_Ioo_iff {α : Type u_1} [Semiring α] [LinearOrder α] [FloorSemiring α] {a b : α} {n : ℕ} (ha : 0 ≤ a) : ↑n ∈ Set.Ioo a b ↔ n ∈ Finset.Ioo ⌊a⌋₊ ⌈b⌉₊

theorem Nat.cast_mem_Iic_iff {α : Type u_1} [Semiring α] [LinearOrder α] [FloorSemiring α] {b : α} {n : ℕ} (hb : 0 ≤ b) : ↑n ∈ Set.Iic b ↔ n ∈ Finset.Iic ⌊b⌋₊

theorem Nat.cast_mem_Iio_iff {α : Type u_1} [Semiring α] [LinearOrder α] [FloorSemiring α] {b : α} {n : ℕ} : ↑n ∈ Set.Iio b ↔ n ∈ Finset.Iio ⌈b⌉₊

theorem Nat.cast_mem_Ioi_iff {α : Type u_1} [Semiring α] [LinearOrder α] [FloorSemiring α] {a : α} {n : ℕ} (ha : 0 ≤ a) : ↑n ∈ Set.Ioi a ↔ n ∈ Set.Ioi ⌊a⌋₊

theorem Nat.cast_mem_Ici_iff {α : Type u_1} [Semiring α] [LinearOrder α] [FloorSemiring α] {a : α} {n : ℕ} : ↑n ∈ Set.Ici a ↔ n ∈ Set.Ici ⌈a⌉₊