Description: The set of closed intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007) (Revised by Mario Carneiro, 3-Nov-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | iccf | ⊢ [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-icc | ⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ) | |
| 2 | 1 | ixxf | ⊢ [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* |