Theory real_topology

⊢ ∀l. interval l = {x | FST (HD l) ≤ x ∧ x ≤ SND (HD l)}

⊢ ∀a b. interval (a,b) = {x | a < x ∧ x < b}

⊢ ball = mball mr1

⊢ ∀x a b. between x (a,b) ⇔ dist (a,b) = dist (a,x) + dist (x,b)

⊢ ∀f. bilinear f ⇔ (∀x. linear (λy. f x y)) ∧ ∀y. linear (λx. f x y)

⊢ ∀s. bounded s ⇔ ∃a. ∀x. x ∈ s ⇒ abs x ≤ a

⊢ ∀s. cauchy s ⇔ ∀e. 0 < e ⇒ ∃N. ∀m n. m ≥ N ∧ n ≥ N ⇒ dist (s m,s n) < e

⊢ cball = mcball mr1

⊢ ∀l. segment l = {(1 − u) * FST (HD l) + u * SND (HD l) | 0 ≤ u ∧ u ≤ 1}

⊢ ∀s a. closest_point s a = @x. x ∈ s ∧ ∀y. y ∈ s ⇒ dist (a,x) ≤ dist (a,y)

⊢ ∀s. closure s = euclidean closure_of s

⊢ ∀s. collinear s ⇔ ∃u. ∀x y. x ∈ s ∧ y ∈ s ⇒ ∃c. x − y = c * u

⊢ ∀s. compact s ⇔
      ∀f. (∀n. f n ∈ s) ⇒
          ∃l r.
            l ∈ s ∧ (∀m n. m < n ⇒ r m < r n) ∧ (f ∘ r ⟶ l) sequentially

⊢ ∀s. complete s ⇔
      ∀f. (∀n. f n ∈ s) ∧ cauchy f ⇒ ∃l. l ∈ s ∧ (f ⟶ l) sequentially

⊢ ∀s. components s = {connected_component s x | x | x ∈ s}

⊢ ∀x s.
    x condensation_point_of s ⇔ ∀t. x ∈ t ∧ open t ⇒ uncountable (s ∩ t)

⊢ ∀s. connected s ⇔
      ¬∃e1 e2.
        open e1 ∧ open e2 ∧ s ⊆ e1 ∪ e2 ∧ e1 ∩ e2 ∩ s = ∅ ∧ e1 ∩ s ≠ ∅ ∧
        e2 ∩ s ≠ ∅

⊢ ∀s x y.
    connected_component s x y ⇔ ∃t. connected t ∧ t ⊆ s ∧ x ∈ t ∧ y ∈ t

⊢ ∀s. content s =
      if s = ∅ then 0 else interval_upperbound s − interval_lowerbound s

⊢ ∀f net. f continuous net ⇔ (f ⟶ f (netlimit net)) net

⊢ ∀f s. f continuous_on s ⇔ ∀x. x ∈ s ⇒ f continuous (at x within s)

⊢ ∀s. dependent s ⇔ ∃a. a ∈ s ∧ a ∈ span (s DELETE a)

⊢ ∀v. dim v = @n. ∃b. b ⊆ v ∧ independent b ∧ v ⊆ span b ∧ b HAS_SIZE n

⊢ closed = closed_in euclidean

⊢ euclidean = mtop mr1

⊢ open = open_in euclidean

⊢ ∀s. frontier s = euclidean frontier_of s

⊢ ∀s t.
    hausdist (s,t) =
    if
      {setdist ({x},t) | x ∈ s} ∪ {setdist ({y},s) | y ∈ t} ≠ ∅ ∧
      ∃b. ∀d.
        d ∈ {setdist ({x},t) | x ∈ s} ∪ {setdist ({y},s) | y ∈ t} ⇒ d ≤ b
    then
      sup ({setdist ({x},t) | x ∈ s} ∪ {setdist ({y},s) | y ∈ t})
    else 0

⊢ ∀s t. s homeomorphic t ⇔ ∃f g. homeomorphism (s,t) (f,g)

⊢ ∀s t f g.
    homeomorphism (s,t) (f,g) ⇔
    (∀x. x ∈ s ⇒ g (f x) = x) ∧ IMAGE f s = t ∧ f continuous_on s ∧
    (∀y. y ∈ t ⇒ f (g y) = y) ∧ IMAGE g t = s ∧ g continuous_on t

⊢ ∀s. independent s ⇔ ¬dependent s

⊢ ∀s. interior s = euclidean interior_of s

⊢ ∀s. interval_lowerbound s = if s = ∅ then 0 else inf s

⊢ ∀s. interval_upperbound s = if s = ∅ then 0 else sup s

⊢ ∀s. is_interval s ⇔
      ∀a b x. a ∈ s ∧ b ∈ s ⇒ a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a ⇒ x ∈ s

⊢ ∀x s. x limit_point_of s ⇔ limpt euclidean x s

⊢ ∀f. linear f ⇔ (∀x y. f (x + y) = f x + f y) ∧ ∀c x. f (c * x) = c * f x

⊢ ∀P s.
    locally P s ⇔
    ∀w x.
      open_in (subtopology euclidean s) w ∧ x ∈ w ⇒
      ∃u v.
        open_in (subtopology euclidean s) u ∧ P v ∧ x ∈ u ∧ u ⊆ v ∧ v ⊆ w

⊢ ∀a b. midpoint (a,b) = 2⁻¹ * (a + b)

⊢ ∀a b. segment (a,b) = segment [(a,b)] DIFF {a; b}

⊢ ∀net f. lim net f = @l. (f ⟶ l) net

⊢ ∀d s.
    set_diameter d s =
    if s = ∅ then 0 else sup {dist d (x,y) | x ∈ s ∧ y ∈ s}

⊢ ∀s. span s = subspace hull s

⊢ ∀x e. sphere (x,e) = {y | dist (x,y) = e}

⊢ ∀s. subspace s ⇔
      0 ∈ s ∧ (∀x y. x ∈ s ∧ y ∈ s ⇒ x + y ∈ s) ∧ ∀c x. x ∈ s ⇒ c * x ∈ s

⊢ ∀s f. suminf s f = @l. (f sums l) s

⊢ ∀s f. summable s f ⇔ ∃l. (f sums l) s

⊢ ∀f l s. (f sums l) s ⇔ ((λn. sum (s ∩ {0 .. n}) f) ⟶ l) sequentially

⊢ ∀f s.
    f uniformly_continuous_on s ⇔
    ∀e. 0 < e ⇒
        ∃d. 0 < d ∧
            ∀x x'. x ∈ s ∧ x' ∈ s ∧ dist (x',x) < d ⇒ dist (f x',f x) < e

⊢ ∀x y.
    abs (x * y) = abs x * abs y ⇔
    abs x * y = abs y * x ∨ abs x * y = -abs y * x

⊢ ∀x y. x * y = abs x * abs y ⇔ abs x * y = abs y * x

⊢ ∀x y. abs (x * y) = abs x * abs y ⇔ collinear {0; x; y}

⊢ ∀e. 0 < e ⇒
      (P ⇒ abs (sum (s ∩ {m .. n}) f) < e ⇔
       P ⇒ n < m ∨ abs (sum (s ∩ {m .. n}) f) < e)

⊢ ∀x y. abs (x + y) = abs x + abs y ⇔ abs x * y = abs y * x

⊢ ∀x y. abs x + abs y ≤ e ⇒ abs (x + y) ≤ e

⊢ ∀m c.
    m ≠ 0 ⇒
    (λx. m * x + c) ∘ (λx. m⁻¹ * x + -(m⁻¹ * c)) = (λx. x) ∧
    (λx. m⁻¹ * x + -(m⁻¹ * c)) ∘ (λx. m * x + c) = (λx. x)

⊢ ∀P Q. (∀x. P x) ∧ (∀x. Q x) ⇔ ∀x. P x ∧ Q x

⊢ ∀P f. (∃d. 0 < d ∧ ∀x. f x < d ⇒ P x) ⇔ ∃d. 0 < d ∧ ∀x. f x ≤ d ⇒ P x

⊢ ∀g s.
    locally compact s ∧ countable g ∧
    (∀t. t ∈ g ⇒ open_in (subtopology euclidean s) t ∧ s ⊆ closure t) ⇒
    s ⊆ closure (BIGINTER g)

⊢ ∀g s.
    locally compact s ∧ s ≠ ∅ ∧ countable g ∧ BIGUNION g = s ⇒
    ∃t u. t ∈ g ∧ open_in (subtopology euclidean s) u ∧ u ⊆ closure t

⊢ ∀x r.
    cball (x,r) = interval [(x − r,x + r)] ∧
    ball (x,r) = interval (x − r,x + r)

⊢ ∀x e. e ≤ 0 ⇒ ball (x,e) = ∅

⊢ ∀x e. ball (x,e) = ∅ ⇔ e ≤ 0

⊢ ∀x e. ball (x,e) = interval (x − e,x + e)

⊢ ∀e. ball (0,e) = interval (-e,e)

⊢ ∀f x r.
    linear f ∧ (∀y. ∃x. f x = y) ∧ (∀x. abs (f x) = abs x) ⇒
    ball (f x,r) = IMAGE f (ball (x,r))

⊢ ∀a r s. ball (a,max r s) = ball (a,r) ∪ ball (a,s)

⊢ ∀a r s. ball (a,min r s) = ball (a,r) ∩ ball (a,s)

⊢ ∀c. 0 < c ⇒ ∀x r. ball (c * x,c * r) = IMAGE (λx. c * x) (ball (x,r))

⊢ ∀x e. ball (x,e) ⊆ cball (x,e)

⊢ ∀a x r. ball (a + x,r) = IMAGE (λy. a + y) (ball (x,r))

⊢ ∀x. ball (x,0) = ∅

⊢ ∀a r. ball (a,r) ∪ sphere (a,r) = cball (a,r)

⊢ ∀f s c.
    complete s ∧ s ≠ ∅ ∧ 0 ≤ c ∧ c < 1 ∧ IMAGE f s ⊆ s ∧
    (∀x y. x ∈ s ∧ y ∈ s ⇒ dist (f x,f y) ≤ c * dist (x,y)) ⇒
    ∃!x. x ∈ s ∧ f x = x

⊢ ∀v b. b ⊆ v ∧ v ⊆ span b ∧ independent b ⇒ FINITE b ∧ CARD b = dim v

⊢ ∀v. ∃b. b ⊆ v ∧ independent b ∧ v ⊆ span b ∧ b HAS_SIZE dim v

⊢ ∀v b. independent b ∧ span b = v ⇒ b HAS_SIZE dim v

⊢ ∀a b x. between x (a,b) ⇔ abs (x − a) * (b − x) = abs (b − x) * (x − a)

⊢ ∀a b c. between a (b,c) ∧ between b (a,c) ⇒ a = b

⊢ ∀a b x. between x (a,b) ⇒ collinear {a; x; b}

⊢ ∀x a b. between x (a,b) ⇔ x ∈ segment [(a,b)]

⊢ ∀a b. between (midpoint (a,b)) (a,b) ∧ between (midpoint (a,b)) (b,a)

⊢ ∀a b. between a (a,b) ∧ between b (a,b) ∧ between a (a,a)

⊢ ∀a x. between x (a,a) ⇔ x = a

⊢ ∀a b x. between x (a,b) ⇔ between x (b,a)

⊢ ∀a b c d. between a (b,c) ∧ between d (a,c) ⇒ between d (b,c)

⊢ ∀a b c d. between a (b,c) ∧ between d (a,b) ⇒ between a (c,d)

⊢ ∀u. u = BIGUNION (components u)

⊢ ∀s. BIGUNION {connected_component s x | x | x ∈ s} = s

⊢ ∀s t. BIGUNION s DIFF t = BIGUNION {x DIFF t | x ∈ s}

⊢ (∀x. x ∈ s ⇒ ∃y. y ∈ t ∧ x ⊆ y) ⇒ BIGUNION s ⊆ BIGUNION t

⊢ (∀x. x ∈ s ⇒ f x ⊆ g x) ⇒ BIGUNION (IMAGE f s) ⊆ BIGUNION (IMAGE g s)

⊢ ∀h. bilinear h ⇒ ∃B. ∀x y. abs (h x y) ≤ B * abs x * abs y

⊢ ∀h. bilinear h ⇒ ∃B. 0 < B ∧ ∀x y. abs (h x y) ≤ B * abs x * abs y

⊢ ∀net f g h.
    f continuous net ∧ g continuous net ∧ bilinear h ⇒
    (λx. h (f x) (g x)) continuous net

⊢ ∀f g h s.
    f continuous_on s ∧ g continuous_on s ∧ bilinear h ⇒
    (λx. h (f x) (g x)) continuous_on s

⊢ bilinear (λx y. x * y)

⊢ ∀h x y z. bilinear h ⇒ h (x + y) z = h x z + h y z

⊢ ∀h c x y. bilinear h ⇒ h (c * x) y = c * h x y

⊢ ∀h x y. bilinear h ⇒ h (-x) y = -h x y

⊢ ∀h x y z. bilinear h ⇒ h (x − y) z = h x z − h y z

⊢ ∀h x. bilinear h ⇒ h 0 x = 0

⊢ ∀h x y z. bilinear h ⇒ h x (y + z) = h x y + h x z

⊢ ∀h c x y. bilinear h ⇒ h x (c * y) = c * h x y

⊢ ∀h x y. bilinear h ⇒ h x (-y) = -h x y

⊢ ∀h x y z. bilinear h ⇒ h x (y − z) = h x y − h x z

⊢ ∀h x. bilinear h ⇒ h x 0 = 0

⊢ ∀h. bilinear h ∧ FINITE s ∧ FINITE t ⇒
      h (sum s f) (sum t g) = sum (s × t) (λ(i,j). h (f i) (g j))

⊢ ∀f g h m n.
    bilinear h ⇒
    sum {m .. n} (λk. h (f k) (g k − g (k − 1))) =
    if m ≤ n then
      h (f (n + 1)) (g n) − h (f m) (g (m − 1)) −
      sum {m .. n} (λk. h (f (k + 1) − f k) (g k))
    else 0

⊢ ∀f g h m n.
    bilinear h ⇒
    sum {m .. n} (λk. h (f k) (g (k + 1) − g k)) =
    if m ≤ n then
      h (f (n + 1)) (g (n + 1)) − h (f m) (g m) −
      sum {m .. n} (λk. h (f (k + 1) − f k) (g (k + 1)))
    else 0

⊢ ∀op. bilinear (λx y. op y x) ⇔ bilinear op

⊢ ∀f g h s.
    f uniformly_continuous_on s ∧ g uniformly_continuous_on s ∧
    bilinear h ∧ bounded (IMAGE f s) ∧ bounded (IMAGE g s) ⇒
    (λx. h (f x) (g x)) uniformly_continuous_on s

⊢ ∀s. bounded s ∧ INFINITE s ⇒ ∃x. x limit_point_of s

⊢ ∀s t. compact s ∧ t ⊆ s ∧ (∀x. x ∈ s ⇒ ¬(x limit_point_of t)) ⇒ FINITE t

⊢ ∀s. (∀t. INFINITE t ∧ t ⊆ s ⇒ ∃x. x limit_point_of t) ⇒ bounded s

⊢ ∀s. (∀t. INFINITE t ∧ t ⊆ s ⇒ ∃x. x ∈ s ∧ x limit_point_of t) ⇒ closed s

⊢ ∀x e. bounded (ball (x,e))

⊢ ∀f. (∃s. s ∈ f ∧ bounded s) ⇒ bounded (BIGINTER f)

⊢ ∀f. FINITE f ∧ (∀s. s ∈ f ⇒ bounded s) ⇒ bounded (BIGUNION f)

⊢ ∀x e. bounded (cball (x,e))

⊢ ∀f b.
    (∀s. s ∈ f ⇒ closed s ∧ s ≠ ∅) ∧
    (∀s t. s ∈ f ∧ t ∈ f ⇒ s ⊆ t ∨ t ⊆ s) ∧ b ∈ f ∧ bounded b ⇒
    BIGINTER f ≠ ∅

⊢ ∀s. bounded s ∧ closed s ⇒ compact s

⊢ ∀a b. bounded (interval [(a,b)])

⊢ ∀s. (∀n. closed (s n)) ∧ (∀n. s n ≠ ∅) ∧ (∀m n. m ≤ n ⇒ s n ⊆ s m) ∧
      bounded (s 0) ⇒
      ∃a. ∀n. a ∈ s n

⊢ ∀s. bounded s ⇒ bounded (closure s)

⊢ ∀s. bounded (closure s) ⇔ bounded s

⊢ ∀s. bounded s ⇔ bounded (IMAGE (λx. x) s)

⊢ ∀s. bounded {s n | n ∈ 𝕌(:num)} ∧ (∀n. s (SUC n) ≤ s n) ⇒
      ∃l. (s ⟶ l) sequentially

⊢ ∀s t. bounded s ⇒ bounded (s DIFF t)

⊢ ∀s t. bounded s ∧ bounded t ⇒ bounded {x − y | x ∈ s ∧ y ∈ t}

⊢ bounded ∅

⊢ ∀s. bounded s ⇔ ∀t. t ⊆ s ∧ INFINITE t ⇒ ∃x. x limit_point_of t

⊢ ∀s. bounded s ⇒ bounded (frontier s)

⊢ ∀s. bounded s ∧ s ≠ ∅ ⇒
      (∀x. x ∈ s ⇒ inf s ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ inf s

⊢ ∀s. bounded s ∧ s ≠ ∅ ⇒
      (∀x. x ∈ s ⇒ x ≤ sup s) ∧ ∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇒ sup s ≤ b

⊢ ∀s. bounded {s n | n ∈ 𝕌(:num)} ∧ (∀n. s n ≤ s (SUC n)) ⇒
      ∃l. (s ⟶ l) sequentially

⊢ ∀x s. bounded (x INSERT s) ⇔ bounded s

⊢ ∀s t. bounded s ∨ bounded t ⇒ bounded (s ∩ t)

⊢ ∀s. bounded s ⇒ bounded (interior s)

⊢ (∀a b. bounded (interval [(a,b)])) ∧ ∀a b. bounded (interval (a,b))

⊢ ∀f s. bounded s ∧ linear f ⇒ bounded (IMAGE f s)

⊢ ∀s. bounded s ⇒ bounded (IMAGE (λx. -x) s)

⊢ ∀f k.
    bounded {sum {k .. n} f | n ∈ 𝕌(:num)} ⇒
    bounded {sum {m .. n} f | m ∈ 𝕌(:num) ∧ n ∈ 𝕌(:num)}

⊢ ∀s. bounded s ⇔ ∃b. 0 < b ∧ ∀x. x ∈ s ⇒ abs x ≤ b

⊢ ∀s. bounded s ⇔ ∃b. 0 < b ∧ ∀x. x ∈ s ⇒ abs x < b

⊢ ∀c s. bounded s ⇒ bounded (IMAGE (λx. c * x) s)

⊢ ∀a. bounded {a}

⊢ ∀a r. bounded (sphere (a,r))

⊢ ∀s t. bounded t ∧ s ⊆ t ⇒ bounded s

⊢ ∀s x. bounded s ⇒ ∃r. 0 < r ∧ s ⊆ ball (x,r)

⊢ ∀s x. bounded s ⇒ ∃r. 0 < r ∧ s ⊆ cball (x,r)

⊢ ∀s. bounded s ⇒ ∃a b. s ⊆ interval [(a,b)]

⊢ ∀s. bounded s ⇒ ∃a. s ⊆ interval [(-a,a)]

⊢ ∀s. bounded s ⇒ ∃a b. s ⊆ interval (a,b)

⊢ ∀s. bounded s ⇒ ∃a. s ⊆ interval (-a,a)

⊢ ∀s t. bounded s ∧ bounded t ⇒ bounded {x + y | x ∈ s ∧ y ∈ t}

⊢ ∀f g t.
    bounded {f x | x ∈ t} ∧ bounded {g x | x ∈ t} ⇒
    bounded {f x + g x | x ∈ t}

⊢ ∀f t s.
    FINITE s ∧ (∀a. a ∈ s ⇒ bounded {f x a | x ∈ t}) ⇒
    bounded {sum s (f x) | x ∈ t}

⊢ ∀a s. bounded s ⇒ bounded (IMAGE (λx. a + x) s)

⊢ ∀a s. bounded (IMAGE (λx. a + x) s) ⇔ bounded s

⊢ ∀f s. f uniformly_continuous_on s ∧ bounded s ⇒ bounded (IMAGE f s)

⊢ ∀s t. bounded (s ∪ t) ⇔ bounded s ∧ bounded t

⊢ ∀a r. 0 < r ⇒ ball (a,r) ≈ 𝕌(:real)

⊢ ∀a r. 0 < r ⇒ cball (a,r) ≈ 𝕌(:real)

⊢ 𝕌(:real) ≈ 𝕌(:real)

⊢ (∀a b. interval (a,b) ≠ ∅ ⇒ interval [(a,b)] ≈ 𝕌(:real)) ∧
  ∀a b. interval (a,b) ≠ ∅ ⇒ interval (a,b) ≈ 𝕌(:real)

⊢ ∀s. open s ∧ s ≠ ∅ ⇒ s ≈ 𝕌(:real)

⊢ 𝕌(:real) ≈ 𝕌(:num -> bool)

⊢ ∀s. s ≈ 𝕌(:real) ⇒ uncountable s

⊢ ∀s. is_interval s ⇒ FINITE (frontier s) ∧ CARD (frontier s) ≤ 2

⊢ ∀v b. b ⊆ v ∧ independent b ∧ dim v ≤ CARD b ⇒ v ⊆ span b

⊢ CARD {1} = 1

⊢ ∀s. cauchy s ⇔ ∀e. 0 < e ⇒ ∃N. ∀n. n ≥ N ⇒ dist (s n,s N) < e

⊢ ∀f s.
    (∀x. cauchy x ∧ (∀n. x n ∈ s) ⇒ cauchy (f ∘ x)) ⇒
    ∃g. g continuous_on closure s ∧ ∀x. x ∈ s ⇒ g x = f x

⊢ ∀f s. (∀x. cauchy x ∧ (∀n. x n ∈ s) ⇒ cauchy (f ∘ x)) ⇒ f continuous_on s

⊢ ∀f s.
    (∀x. cauchy x ∧ (∀n. x n ∈ s) ⇒ cauchy (f ∘ x)) ⇒
    ∀a x.
      (∀n. x n ∈ s) ∧ (x ⟶ a) sequentially ⇒
      ∃l. (f ∘ x ⟶ l) sequentially ∧
          ∀y. (∀n. y n ∈ s) ∧ (y ⟶ a) sequentially ⇒
              (f ∘ y ⟶ l) sequentially

⊢ ∀s. cauchy s ⇒ bounded {y | (∃n. y = s n)}

⊢ ∀f s e x.
    0 < e ∧ subspace s ∧ linear f ∧ (∀x. x ∈ s ⇒ abs (f x) ≥ e * abs x) ∧
    (∀n. x n ∈ s) ∧ cauchy (f ∘ x) ⇒
    cauchy x

⊢ ∀a r. cball (a,r) DIFF ball (a,r) = sphere (a,r)

⊢ ∀a r. cball (a,r) DIFF sphere (a,r) = ball (a,r)

⊢ ∀x e. e < 0 ⇒ cball (x,e) = ∅

⊢ ∀x e. cball (x,e) = ∅ ⇔ e < 0

⊢ ∀x e. cball (x,e) = {x} ⇔ e = 0

⊢ ∀x e. cball (x,e) = interval [(x − e,x + e)]

⊢ ∀e. cball (0,e) = interval [(-e,e)]

⊢ ∀f x r.
    linear f ∧ (∀y. ∃x. f x = y) ∧ (∀x. abs (f x) = abs x) ⇒
    cball (f x,r) = IMAGE f (cball (x,r))

⊢ ∀a r s. cball (a,max r s) = cball (a,r) ∪ cball (a,s)

⊢ ∀x d e. cball (x,min d e) = cball (x,d) ∩ cball (x,e)

⊢ ∀c. 0 < c ⇒ ∀x r. cball (c * x,c * r) = IMAGE (λx. c * x) (cball (x,r))

⊢ ∀x e. e = 0 ⇒ cball (x,e) = {x}

⊢ ∀a x r. cball (a + x,r) = IMAGE (λy. a + y) (cball (x,r))

⊢ ∀x. cball (x,0) = {x}

⊢ ∀x e. x ∈ ball (x,e) ⇔ 0 < e

⊢ ∀x e. x ∈ cball (x,e) ⇔ 0 ≤ e

⊢ ∀s. closed s ∧ open s ⇔ s = ∅ ∨ s = 𝕌(:real)

⊢ ∀u s.
    closed_in (subtopology euclidean u) s ∧
    open_in (subtopology euclidean u) s ⇒
    ∃k. k ⊆ components u ∧ s = BIGUNION k

⊢ ∀u s.
    closed_in (subtopology euclidean u) s ∧
    open_in (subtopology euclidean u) s ∧ connected s ∧ s ≠ ∅ ⇒
    s ∈ components u

⊢ ∀s. closed s ⇔
      ∀x. (∀e. 0 < e ⇒ ∃x'. x' ∈ s ∧ x' ≠ x ∧ abs (x' − x) < e) ⇒ x ∈ s

⊢ ∀x s. closed s ⇒ ((∀e. 0 < e ⇒ ∃y. y ∈ s ∧ dist (y,x) < e) ⇔ x ∈ s)

⊢ ∀s. closed s ⇒ gdelta s

⊢ ∀f. (∀s. s ∈ f ⇒ closed s) ⇒ closed (BIGINTER f)

⊢ ∀s. closed s ⇔ ∀e. compact (cball (0,e) ∩ s)

⊢ ∀s. FINITE s ∧ (∀t. t ∈ s ⇒ closed t) ⇒ closed (BIGUNION s)

⊢ ∀x e. closed (cball (x,e))

⊢ ∀s. closed (closure s)

⊢ ∀s t. closed s ∧ compact t ⇒ closed {x − y | x ∈ s ∧ y ∈ t}

⊢ ∀s t. closed s ∧ compact t ⇒ closed {x + y | x ∈ s ∧ y ∈ t}

⊢ ∀s c. closed s ∧ c ∈ components s ⇒ closed c

⊢ ∀s x. closed s ⇒ closed (connected_component s x)

⊢ ∀s x l. closed s ∧ (∀n. x n ∈ s) ∧ (x ⟶ l) sequentially ⇒ l ∈ s

⊢ ∀s t. closed s ∧ open t ⇒ closed (s DIFF t)

⊢ ∀a b.
    interval [(a,b)] DIFF interval (a,b) =
    if interval [(a,b)] = ∅ then ∅ else {a; b}

⊢ closed ∅

⊢ ∀f. (∀t. t ∈ f ⇒ closed t) ∧ (∃t. t ∈ f ∧ bounded t) ∧
      (∀f'. FINITE f' ∧ f' ⊆ f ⇒ BIGINTER f' ≠ ∅) ⇒
      BIGINTER f ≠ ∅

⊢ ∀Q. (∀a. closed {x | Q a x}) ⇒ closed {x | (∀a. Q a x)}

⊢ ∀P Q. (∀a. P a ⇒ closed {x | Q a x}) ⇒ closed {x | (∀a. P a ⇒ Q a x)}

⊢ ∀a. closed {x | x ≥ a}

⊢ ∀a. closed {x | x ≤ a}

⊢ ∀a b. closed {x | a * x ≥ b}

⊢ ∀a b. closed {x | a * x ≤ b}

⊢ ∀a b. closed {x | a * x = b}

⊢ ∀s f.
    closed s ∧ (∀t. t ∈ f ⇒ closed t) ∧ (∃t. t ∈ f ∧ bounded t) ∧
    (∀f'. FINITE f' ∧ f' ⊆ f ⇒ s ∩ BIGINTER f' ≠ ∅) ⇒
    s ∩ BIGINTER f ≠ ∅

⊢ ∀s f.
    closed s ∧ (∀t. t ∈ f ⇒ compact t) ∧
    (∀f'. FINITE f' ∧ f' ⊆ f ⇒ s ∩ BIGINTER f' ≠ ∅) ⇒
    s ∩ BIGINTER f ≠ ∅

⊢ ∀s. closed s ⇒ locally compact s

⊢ ∀s. closed s ⇔ closed_in euclidean s

⊢ ∀f s.
    subspace s ∧ linear f ∧ (∀x. x ∈ s ∧ f x = 0 ⇒ x = 0) ∧ closed s ⇒
    closed (IMAGE f s)

⊢ ∀f. linear f ∧ (∀x y. f x = f y ⇒ x = y) ⇒
      ∀s. closed s ⇒ closed (IMAGE f s)

⊢ ∀f s.
    linear f ∧ (∀x y. f x = f y ⇒ x = y) ⇒ (closed (IMAGE f s) ⇔ closed s)

⊢ ∀a s. closed s ⇒ closed (a INSERT s)

⊢ ∀s t. closed s ∧ closed t ⇒ closed (s ∩ t)

⊢ ∀a b. closed (interval [(a,b)])

⊢ (∀a b. closed (interval [(a,b)])) ∧
  ∀a b. closed (interval (a,b)) ⇔ interval (a,b) = ∅

⊢ ∀a b.
    interval [(a,b)] ≠ ∅ ⇒
    interval [(a,b)] =
    IMAGE (λx. a + x) (IMAGE (λx. @f. f = (b − a) * x) (interval [(0,1)]))

⊢ ∀b. closed {x | x ≤ b}

⊢ ∀a. closed {x | a ≤ x}

⊢ ∀s t. closed s ∧ compact t ⇒ compact (s ∩ t)

⊢ ∀s u. closed_in (subtopology euclidean u) s ⇔ ∃t. closed t ∧ s = u ∩ t

⊢ ∀s t.
    closed s ⇒ (closed_in (subtopology euclidean s) t ⇔ closed t ∧ t ⊆ s)

⊢ ∀u s. closed s ⇒ closed_in (subtopology euclidean u) (u ∩ s)

⊢ ∀s t. closed_in (subtopology euclidean t) s ∧ closed t ⇒ closed s

⊢ ∀s t. compact s ∧ closed_in (subtopology euclidean s) t ⇒ compact t

⊢ ∀s t.
    compact s ⇒ (closed_in (subtopology euclidean s) t ⇔ compact t ∧ t ⊆ s)

⊢ ∀s c. c ∈ components s ⇒ closed_in (subtopology euclidean s) c

⊢ ∀s x. closed_in (subtopology euclidean s) (connected_component s x)

⊢ ∀s t u.
    closed_in (subtopology euclidean u) s ∧ closed t ⇒
    closed_in (subtopology euclidean u) (s ∩ t)

⊢ ∀s t. closed_in (subtopology euclidean s) t ⇔ s ∩ closure t = t

⊢ ∀s t.
    closed_in (subtopology euclidean t) s ⇔
    s ⊆ t ∧ ∀x. x limit_point_of s ∧ x ∈ t ⇒ x ∈ s

⊢ ∀s. closed_in (subtopology euclidean s) s

⊢ ∀u x. closed_in (subtopology euclidean u) {x} ⇔ x ∈ u

⊢ ∀s t u.
    closed_in (subtopology euclidean u) s ∧ s ⊆ t ∧ t ⊆ u ⇒
    closed_in (subtopology euclidean t) s

⊢ ∀s t u.
    closed_in (subtopology euclidean t) s ∧
    closed_in (subtopology euclidean u) t ⇒
    closed_in (subtopology euclidean u) s

⊢ ∀s t.
    (∀u. closed_in (subtopology euclidean t) u ⇒
         closed_in (subtopology euclidean s) t) ⇔
    closed_in (subtopology euclidean s) t

⊢ ∀s. closed s ⇔ ∀x. x limit_point_of s ⇒ x ∈ s

⊢ ∀s. closed {x | x limit_point_of s}

⊢ ∀f. (∀s. closed s ⇒ closed (IMAGE f s)) ⇔
      ∀s. closure (IMAGE f s) ⊆ IMAGE f (closure s)

⊢ ∀f g s t u.
    IMAGE f s ⊆ t ∧ IMAGE g t ⊆ u ∧ g continuous_on t ∧
    (∀x y. x ∈ t ∧ y ∈ t ∧ g x = g y ⇒ x = y) ∧
    (∀k. closed_in (subtopology euclidean s) k ⇒
         closed_in (subtopology euclidean u) (IMAGE (g ∘ f) k)) ⇒
    ∀k. closed_in (subtopology euclidean s) k ⇒
        closed_in (subtopology euclidean t) (IMAGE f k)

⊢ ∀f g s t u.
    f continuous_on s ∧ IMAGE f s = t ∧ IMAGE g t ⊆ u ∧
    (∀k. closed_in (subtopology euclidean s) k ⇒
         closed_in (subtopology euclidean u) (IMAGE (g ∘ f) k)) ⇒
    ∀k. closed_in (subtopology euclidean t) k ⇒
        closed_in (subtopology euclidean u) (IMAGE g k)

⊢ ∀f s t.
    IMAGE f s ⊆ t ⇒
    ((∀u. closed_in (subtopology euclidean s) u ⇒
          closed_in (subtopology euclidean t) (IMAGE f u)) ⇔
     ∀u. open_in (subtopology euclidean s) u ⇒
         open_in (subtopology euclidean t)
           {y | y ∈ t ∧ {x | x ∈ s ∧ f x = y} ⊆ u})

⊢ ∀f s t.
    IMAGE f s = t ∧
    (∀u. closed_in (subtopology euclidean s) u ⇒
         closed_in (subtopology euclidean t) (IMAGE f u)) ∧
    (∀u. open_in (subtopology euclidean s) u ⇒
         open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ IMAGE f u}) ⇒
    ∀u. open_in (subtopology euclidean s) u ⇒
        open_in (subtopology euclidean t) (IMAGE f u)

⊢ ∀f s.
    f continuous_on s ∧
    (∀t. closed_in (subtopology euclidean s) t ⇒
         closed_in (subtopology euclidean (IMAGE f s)) (IMAGE f t)) ⇒
    ∀t. t ⊆ IMAGE f s ⇒
        (open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ t} ⇔
         open_in (subtopology euclidean (IMAGE f s)) t)

⊢ ∀f s t u w.
    (∀k. closed_in (subtopology euclidean s) k ⇒
         closed_in (subtopology euclidean t) (IMAGE f k)) ∧
    open_in (subtopology euclidean s) u ∧ w ⊆ t ∧ {x | x ∈ s ∧ f x ∈ w} ⊆ u ⇒
    ∃v. open_in (subtopology euclidean t) v ∧ w ⊆ v ∧
        {x | x ∈ s ∧ f x ∈ v} ⊆ u

⊢ ∀f s t.
    IMAGE f s ⊆ t ⇒
    ((∀k. closed_in (subtopology euclidean s) k ⇒
          closed_in (subtopology euclidean t) (IMAGE f k)) ⇔
     ∀u w.
       open_in (subtopology euclidean s) u ∧ w ⊆ t ∧
       {x | x ∈ s ∧ f x ∈ w} ⊆ u ⇒
       ∃v. open_in (subtopology euclidean t) v ∧ w ⊆ v ∧
           {x | x ∈ s ∧ f x ∈ v} ⊆ u)

⊢ ∀f s t.
    IMAGE f s ⊆ t ⇒
    ((∀k. closed_in (subtopology euclidean s) k ⇒
          closed_in (subtopology euclidean t) (IMAGE f k)) ⇔
     ∀u y.
       open_in (subtopology euclidean s) u ∧ y ∈ t ∧
       {x | x ∈ s ∧ f x = y} ⊆ u ⇒
       ∃v. open_in (subtopology euclidean t) v ∧ y ∈ v ∧
           {x | x ∈ s ∧ f x ∈ v} ⊆ u)

⊢ ∀f s t t'.
    (∀u. closed_in (subtopology euclidean s) u ⇒
         closed_in (subtopology euclidean t) (IMAGE f u)) ∧ t' ⊆ t ⇒
    ∀u. closed_in (subtopology euclidean {x | x ∈ s ∧ f x ∈ t'}) u ⇒
        closed_in (subtopology euclidean t') (IMAGE f u)

⊢ ∀s. closed s ⇒ closed (IMAGE (λx. -x) s)

⊢ ∀a b. a ≤ b ⇒ interval [(a,b)] = interval (a,b) ∪ {a; b}

⊢ closed {x | 0 ≤ x}

⊢ ∀s c. closed s ⇒ closed (IMAGE (λx. c * x) s)

⊢ ∀f a b. linear f ⇒ segment [(f a,f b)] = IMAGE f (segment [(a,b)])

⊢ ∀s. closed s ⇔ ∀x l. (∀n. x n ∈ s) ∧ (x ⟶ l) sequentially ⇒ l ∈ s

⊢ ∀a. closed {a}

⊢ ∀a r. closed (sphere (a,r))

⊢ ∀a. closed {x | x = a}

⊢ ∀s t. s ⊆ t ∧ closed s ⇒ closed_in (subtopology euclidean t) s

⊢ ∀u s. closed s ⇒ (closed_in (subtopology euclidean u) s ⇔ s ⊆ u)

⊢ closed {x | x = 0}

⊢ ∀s t. closed s ∧ closed t ⇒ closed (s ∪ t)

⊢ ∀s. closed s ⇒
      ∃f. (∀n. compact (f n)) ∧ (∀n. f n ⊆ s) ∧ (∀n. f n ⊆ f (n + 1)) ∧
          BIGUNION {f n | n ∈ 𝕌(:num)} = s ∧
          ∀k. compact k ∧ k ⊆ s ⇒ ∃N. ∀n. n ≥ N ⇒ k ⊆ f n

⊢ closed 𝕌(:real)

⊢ ∀s a.
    closed s ∧ s ≠ ∅ ⇒
    closest_point s a ∈ s ∧
    ∀y. y ∈ s ⇒ dist (a,closest_point s a) ≤ dist (a,y)

⊢ ∀s x. closed s ∧ s ≠ ∅ ∧ x ∉ interior s ⇒ closest_point s x ∈ frontier s

⊢ ∀s x.
    closed s ∧ s ≠ ∅ ⇒ (closest_point s x ∈ interior s ⇔ x ∈ interior s)

⊢ ∀s a. closed s ∧ s ≠ ∅ ⇒ closest_point s a ∈ s

⊢ ∀s a x. closed s ∧ x ∈ s ⇒ dist (a,closest_point s a) ≤ dist (a,x)

⊢ ∀s x. closed s ∧ s ≠ ∅ ⇒ (closest_point s x = x ⇔ x ∈ s)

⊢ ∀s x. x ∈ s ⇒ closest_point s x = x

⊢ ∀x s. x ∈ closure s ⇔ ∀e. 0 < e ⇒ ∃y. y ∈ s ∧ dist (y,x) < e

⊢ ∀x e. 0 < e ⇒ closure (ball (x,e)) = cball (x,e)

⊢ ∀f. closure (BIGINTER f) ⊆ BIGINTER (IMAGE closure f)

⊢ ∀f. FINITE f ⇒ closure (BIGUNION f) = BIGUNION {closure s | s ∈ f}

⊢ ∀f s. linear f ∧ bounded s ⇒ closure (IMAGE f s) = IMAGE f (closure s)

⊢ ∀s. closed s ⇒ closure s = s

⊢ ∀s. closure (closure s) = closure s

⊢ ∀s. closure (𝕌(:real) DIFF s) = 𝕌(:real) DIFF interior s

⊢ closure ∅ = ∅

⊢ ∀s. closure s = s ⇔ closed s

⊢ ∀s. closure s = ∅ ⇔ s = ∅

⊢ ∀a. closure {x | x > a} = {x | x ≥ a}

⊢ ∀a. closure {x | x < a} = {x | x ≤ a}

⊢ ∀a b. a ≠ 0 ⇒ closure {x | a * x > b} = {x | a * x ≥ b}

⊢ ∀a b. a ≠ 0 ⇒ closure {x | a * x < b} = {x | a * x ≤ b}

⊢ ∀s. closure s = closed hull s

⊢ ∀a b. closure {x | a * x = b} = {x | a * x = b}

⊢ ∀f s.
    f continuous_on closure s ∧ bounded s ⇒
    closure (IMAGE f s) = IMAGE f (closure s)

⊢ ∀f s.
    f continuous_on closure s ⇒
    closure (IMAGE f (closure s)) = closure (IMAGE f s)

⊢ ∀f s.
    linear f ∧ (∀x y. f x = f y ⇒ x = y) ⇒
    closure (IMAGE f s) = IMAGE f (closure s)

⊢ ∀s. closure s = 𝕌(:real) DIFF interior (𝕌(:real) DIFF s)

⊢ ∀s. closure (interior (closure (interior s))) = closure (interior s)

⊢ ∀s t.
    closed s ∧ closed t ⇒
    closure (interior (s ∪ t)) =
    closure (interior s) ∪ closure (interior t)

⊢ (∀a b. closure (interval [(a,b)]) = interval [(a,b)]) ∧
  ∀a b.
    closure (interval (a,b)) =
    if interval (a,b) = ∅ then ∅ else interval [(a,b)]

⊢ ∀s t. closure (s ∩ t) ⊆ closure s ∩ closure t

⊢ ∀f s. linear f ⇒ IMAGE f (closure s) ⊆ closure (IMAGE f s)

⊢ ∀s t. s ⊆ t ∧ closed t ⇒ closure s ⊆ t

⊢ ∀s t. closed t ⇒ (closure s ⊆ t ⇔ s ⊆ t)

⊢ ∀s. closure (IMAGE (λx. -x) s) = IMAGE (λx. -x) (closure s)

⊢ ∀s x. x ∈ closure s ⇔ ∀t. x ∈ t ∧ open t ⇒ s ∩ t ≠ ∅

⊢ ∀a b. interval (a,b) ≠ ∅ ⇒ closure (interval (a,b)) = interval [(a,b)]

⊢ ∀s t. open s ⇒ closure (s ∩ closure t) = closure (s ∩ t)

⊢ ∀s t. open s ∧ s ⊆ closure t ⇒ closure (s ∩ t) = closure s

⊢ ∀s t u.
    open_in (subtopology euclidean u) s ∧ t ⊆ u ⇒
    closure (s ∩ closure t) = closure (s ∩ t)

⊢ ∀s l. l ∈ closure s ⇔ ∃x. (∀n. x n ∈ s) ∧ (x ⟶ l) sequentially

⊢ ∀x. closure {x} = {x}

⊢ ∀s. s ⊆ closure s

⊢ ∀s. closure s ⊆ s ⇔ closed s

⊢ ∀s t.
    bounded s ∨ bounded t ⇒
    closure {x + y | x ∈ s ∧ y ∈ t} =
    {x + y | x ∈ closure s ∧ y ∈ closure t}

⊢ ∀s t. closure (s ∪ t) = closure s ∪ closure t

⊢ ∀s. closure s = s ∪ frontier s

⊢ ∀s t.
    s ⊆ t ∧ closed t ∧ (∀t'. s ⊆ t' ∧ closed t' ⇒ t ⊆ t') ⇒ closure s = t

⊢ closure 𝕌(:real) = 𝕌(:real)

⊢ ∀s. bounded (𝕌(:real) DIFF s) ⇒ ¬bounded s

⊢ ∀s t. bounded (𝕌(:real) DIFF s) ∧ ¬bounded t ⇒ s ∩ t ≠ ∅

⊢ ∀s. collinear s

⊢ ∀x y. collinear {x; y}

⊢ ∀x y z. collinear {x; y; z} ⇔ collinear {0; x − y; z − y}

⊢ ∀a b c. collinear {a; b; c} ⇔ a = c ∨ ∃u. b = u * a + (1 − u) * c

⊢ ∀a b c d.
    collinear {a; b; c} ∧ collinear {b; c; d} ∧ b ≠ c ⇒ collinear {a; b; d}

⊢ ∀a b c d.
    a ≠ b ⇒
    (collinear {a; b; c; d} ⇔ collinear {a; b; c} ∧ collinear {a; b; d})

⊢ ∀a b c.
    collinear {a; b; c} ⇔
    between a (b,c) ∨ between b (c,a) ∨ between c (a,b)

⊢ ∀a b x.
    collinear {x; a; b} ∧ dist (x,a) ≤ dist (a,b) ∧ dist (x,b) ≤ dist (a,b) ⇒
    between x (a,b)

⊢ ∀a b x.
    collinear {x; a; b} ∧ dist (x,a) ≤ dist (a,b) ∧ dist (x,b) ≤ dist (a,b) ⇒
    x ∈ segment [(a,b)]

⊢ ∀a b x.
    collinear {x; a; b} ∧ dist (x,a) < dist (a,b) ∧ dist (x,b) < dist (a,b) ⇒
    x ∈ segment (a,b)

⊢ collinear ∅

⊢ ∀x y. collinear {0; x; y} ⇔ x = 0 ∨ y = 0 ∨ ∃c. y = c * x

⊢ ∀x y. collinear {0; x; y} ⇔ x = 0 ∨ ∃c. y = c * x

⊢ ∀a b. collinear {a; midpoint (a,b); b}

⊢ ∀x. collinear {x}

⊢ ∀s. FINITE s ∧ CARD s ≤ 2 ⇒ collinear s

⊢ ∀s t. collinear t ∧ s ⊆ t ⇒ collinear s

⊢ ∀s a b.
    a ≠ b ⇒
    (collinear (a INSERT b INSERT s) ⇔ ∀x. x ∈ s ⇒ collinear {a; b; x})

⊢ ∀s a c. compact s ⇒ compact (IMAGE (λx. a + c * x) s)

⊢ ∀s. compact s ∧ s ≠ ∅ ⇒ ∃x. x ∈ s ∧ ∀y. y ∈ s ⇒ x ≤ y

⊢ ∀s. compact s ∧ s ≠ ∅ ⇒ ∃x. x ∈ s ∧ ∀y. y ∈ s ⇒ y ≤ x

⊢ ∀f. (∀s. s ∈ f ⇒ compact s) ∧ f ≠ ∅ ⇒ compact (BIGINTER f)

⊢ ∀s. FINITE s ∧ (∀t. t ∈ s ⇒ compact t) ⇒ compact (BIGUNION s)

⊢ ∀x e. compact (cball (x,e))

⊢ ∀f. (∀s. s ∈ f ⇒ compact s ∧ s ≠ ∅) ∧
      (∀s t. s ∈ f ∧ t ∈ f ⇒ s ⊆ t ∨ t ⊆ s) ⇒
      BIGINTER f ≠ ∅

⊢ ∀s t. compact s ∧ closed t ⇒ closed {x − y | x ∈ s ∧ y ∈ t}

⊢ ∀s t. compact s ∧ closed t ⇒ closed {x + y | x ∈ s ∧ y ∈ t}

⊢ ∀s. compact (closure s) ⇔ bounded s

⊢ ∀s c. compact s ∧ c ∈ components s ⇒ compact c

⊢ ∀f s. f continuous_on s ∧ compact s ⇒ compact (IMAGE f s)

⊢ ∀f s.
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
    (f continuous_on s ⇔ ∀t. compact t ∧ t ⊆ s ⇒ compact (IMAGE f t))

⊢ ∀s t. compact s ∧ open t ⇒ compact (s DIFF t)

⊢ compact ∅

⊢ ∀s. compact s ⇔ ∀t. INFINITE t ∧ t ⊆ s ⇒ ∃x. x ∈ s ∧ x limit_point_of t

⊢ ∀s. compact s ⇔ bounded s ∧ closed s

⊢ ∀s. compact s ⇔
      ∀f. (∀t. t ∈ f ⇒ open t) ∧ s ⊆ BIGUNION f ⇒
          ∃f'. f' ⊆ f ∧ FINITE f' ∧ s ⊆ BIGUNION f'

⊢ ∀s. compact s ⇔
      ∀f. (∀t. t ∈ f ⇒ open_in (subtopology euclidean s) t) ∧
          s ⊆ BIGUNION f ⇒
          ∃f'. f' ⊆ f ∧ FINITE f' ∧ s ⊆ BIGUNION f'

⊢ ∀f. (∀t. t ∈ f ⇒ compact t) ∧ (∀f'. FINITE f' ∧ f' ⊆ f ⇒ BIGINTER f' ≠ ∅) ⇒
      BIGINTER f ≠ ∅

⊢ ∀s. compact s ⇒ compact (frontier s)

⊢ ∀s. bounded s ⇒ compact (frontier s)

⊢ ∀s. compact s ⇒ bounded s

⊢ ∀s. compact s ⇒ closed s

⊢ ∀s. compact s ⇒ complete s

⊢ ∀s f.
    compact s ∧ (∀t. t ∈ f ⇒ closed t) ∧
    (∀f'. FINITE f' ∧ f' ⊆ f ⇒ s ∩ BIGINTER f' ≠ ∅) ⇒
    s ∩ BIGINTER f ≠ ∅

⊢ ∀s. compact s ⇒
      ∀f. (∀t. t ∈ f ⇒ open t) ∧ s ⊆ BIGUNION f ⇒
          ∃f'. f' ⊆ f ∧ FINITE f' ∧ s ⊆ BIGUNION f'

⊢ ∀s. compact s ⇒
      ∀e. 0 < e ⇒
          ∃k. FINITE k ∧ k ⊆ s ∧ s ⊆ BIGUNION (IMAGE (λx. ball (x,e)) k)

⊢ ∀a s. compact s ⇒ compact (a INSERT s)

⊢ ∀s t. compact s ∧ compact t ⇒ compact (s ∩ t)

⊢ ∀a b. compact (interval [(a,b)])

⊢ (∀a b. compact (interval [(a,b)])) ∧
  ∀a b. compact (interval (a,b)) ⇔ interval (a,b) = ∅

⊢ ∀s t. compact s ∧ closed t ⇒ compact (s ∩ t)

⊢ ∀s. bounded s ∧ (∀n. x n ∈ s) ⇒
      ∃l r.
        (∀m n. m < n ⇒ r m < r n) ∧
        ∀e. 0 < e ⇒ ∃N. ∀n i. N ≤ n ⇒ abs (x (r n) − l) < e

⊢ ∀f s. compact s ∧ linear f ⇒ compact (IMAGE f s)

⊢ ∀s. compact s ⇒ compact (IMAGE (λx. -x) s)

⊢ ∀s. (∀n. compact (s n) ∧ s n ≠ ∅) ∧ (∀m n. m ≤ n ⇒ s n ⊆ s m) ⇒
      BIGINTER {s n | n ∈ 𝕌(:num)} ≠ ∅

⊢ ∀s b.
    (∀n. abs (s n) ≤ b) ⇒
    ∃l r.
      (∀m n. m < n ⇒ r m < r n) ∧
      ∀e. 0 < e ⇒ ∃N. ∀n. N ≤ n ⇒ abs (s (r n) − l) < e

⊢ ∀s c. compact s ⇒ compact (IMAGE (λx. c * x) s)

⊢ ∀f l. (f ⟶ l) sequentially ⇒ compact (l INSERT IMAGE f 𝕌(:num))

⊢ ∀a. compact {a}

⊢ ∀a r. compact (sphere (a,r))

⊢ ∀s a. compact s ⇒ compact (IMAGE (λx. a + x) s)

⊢ ∀a s. compact (IMAGE (λx. a + x) s) ⇔ compact s

⊢ ∀f s. f continuous_on s ∧ compact s ⇒ f uniformly_continuous_on s

⊢ ∀fs s.
    (∀x e.
       x ∈ s ∧ 0 < e ⇒
       ∃d. 0 < d ∧
           ∀f x'. f ∈ fs ∧ x' ∈ s ∧ dist (x',x) < d ⇒ dist (f x',f x) < e) ∧
    compact s ⇒
    ∀e. 0 < e ⇒
        ∃d. 0 < d ∧
            ∀f x x'.
              f ∈ fs ∧ x ∈ s ∧ x' ∈ s ∧ dist (x',x) < d ⇒
              dist (f x',f x) < e

⊢ ∀s t. compact s ∧ compact t ⇒ compact (s ∪ t)

⊢ ∀s x.
    s DIFF connected_component s x =
    BIGUNION
      ({connected_component s y | y | y ∈ s} DELETE connected_component s x)

⊢ ∀s. complete s ⇔ closed s

⊢ ∀f. linear f ∧ (∀x y. f x = f y ⇒ x = y) ⇒
      ∀s. complete s ⇒ complete (IMAGE f s)

⊢ ∀f s.
    linear f ∧ (∀x y. f x = f y ⇒ x = y) ⇒
    (complete (IMAGE f s) ⇔ complete s)

⊢ ∀f s e.
    0 < e ∧ subspace s ∧ linear f ∧ (∀x. x ∈ s ⇒ abs (f x) ≥ e * abs x) ∧
    complete s ⇒
    complete (IMAGE f s)

⊢ complete 𝕌(:real)

⊢ components ∅ = ∅

⊢ ∀s c c'. c ∈ components s ∧ c' ∈ components s ⇒ (c = c' ⇔ c ∩ c' ≠ ∅)

⊢ ∀s. components s = ∅ ⇔ s = ∅

⊢ ∀s. components s = {s} ⇔ connected s ∧ s ≠ ∅

⊢ ∀s. (∃a. components s = {a}) ⇔ connected s ∧ s ≠ ∅

⊢ (∀s. components s = {s} ⇔ connected s ∧ s ≠ ∅) ∧
  ∀s. (∃a. components s = {a}) ⇔ connected s ∧ s ≠ ∅

⊢ ∀s t u. s ∈ components u ∧ s ⊆ t ∧ t ⊆ u ⇒ s ∈ components t

⊢ ∀s t c. c ∈ components s ∧ connected t ∧ t ⊆ s ∧ c ∩ t ≠ ∅ ⇒ t ⊆ c

⊢ ∀s c c'. c ∈ components s ∧ c' ∈ components s ⇒ (c ∩ c' = ∅ ⇔ c ≠ c')

⊢ ∀s k.
    BIGUNION k = s ∧
    (∀c. c ∈ k ⇒
         connected c ∧ c ≠ ∅ ∧ ∀c'. connected c' ∧ c ⊆ c' ∧ c' ⊆ s ⇒ c' = c) ⇒
    components s = k

⊢ ∀s k.
    components s = k ⇔
    BIGUNION k = s ∧
    ∀c. c ∈ k ⇒
        connected c ∧ c ≠ ∅ ∧ ∀c'. connected c' ∧ c ⊆ c' ∧ c' ⊆ s ⇒ c' = c

⊢ components 𝕌(:real) = {𝕌(:real)}

⊢ ∀x s. x condensation_point_of s ⇒ x limit_point_of s

⊢ ∀s x.
    x condensation_point_of s ⇔ ∀e. 0 < e ⇒ uncountable (s ∩ ball (x,e))

⊢ (∀s x.
     x condensation_point_of s ⇔ ∀e. 0 < e ⇒ uncountable (s ∩ ball (x,e))) ∧
  ∀s x.
    x condensation_point_of s ⇔ ∀e. 0 < e ⇒ uncountable (s ∩ cball (x,e))

⊢ ∀s x.
    x condensation_point_of s ⇔ ∀e. 0 < e ⇒ uncountable (s ∩ cball (x,e))

⊢ ∀x s t. x condensation_point_of s ∧ s ⊆ t ⇒ x condensation_point_of t

⊢ ∀P. (∀s. s ∈ P ⇒ connected s) ∧ BIGINTER P ≠ ∅ ⇒ connected (BIGUNION P)

⊢ ∀f. (∀s. s ∈ f ⇒ compact s ∧ connected s) ∧
      (∀s t. s ∈ f ∧ t ∈ f ⇒ s ⊆ t ∨ t ⊆ s) ⇒
      connected (BIGINTER f)

⊢ ∀f. (∀s. s ∈ f ⇒ closed s ∧ connected s) ∧ (∃s. s ∈ f ∧ compact s) ∧
      (∀s t. s ∈ f ∧ t ∈ f ⇒ s ⊆ t ∨ t ⊆ s) ⇒
      connected (BIGINTER f)

⊢ ∀s. connected s ⇔
      ∀t. open_in (subtopology euclidean s) t ∧
          closed_in (subtopology euclidean s) t ⇒
          t = ∅ ∨ t = s

⊢ ∀s. connected s ⇔
      ¬∃e1 e2.
        closed e1 ∧ closed e2 ∧ s ⊆ e1 ∪ e2 ∧ e1 ∩ e2 ∩ s = ∅ ∧
        e1 ∩ s ≠ ∅ ∧ e2 ∩ s ≠ ∅

⊢ ∀s. connected s ⇔
      ¬∃e1 e2.
        closed_in (subtopology euclidean s) e1 ∧
        closed_in (subtopology euclidean s) e2 ∧ s ⊆ e1 ∪ e2 ∧
        e1 ∩ e2 = ∅ ∧ e1 ≠ ∅ ∧ e2 ≠ ∅

⊢ ∀s. connected s ⇔
      ¬∃e1 e2.
        closed_in (subtopology euclidean s) e1 ∧
        closed_in (subtopology euclidean s) e2 ∧ e1 ∪ e2 = s ∧
        e1 ∩ e2 = ∅ ∧ e1 ≠ ∅ ∧ e2 ≠ ∅

⊢ ∀f s t.
    f continuous_on s ∧ IMAGE f s = t ∧
    (∀c. closed_in (subtopology euclidean s) c ⇒
         closed_in (subtopology euclidean t) (IMAGE f c)) ∧
    (∀y. y ∈ t ⇒ connected {x | x ∈ s ∧ f x = y}) ⇒
    ∀c. connected c ∧ c ⊆ t ⇒ connected {x | x ∈ s ∧ f x ∈ c}

⊢ ∀s. closed s ⇒
      (connected s ⇔
       ¬∃e1 e2.
         closed e1 ∧ closed e2 ∧ e1 ≠ ∅ ∧ e2 ≠ ∅ ∧ e1 ∪ e2 = s ∧
         e1 ∩ e2 = ∅)

⊢ ∀s. connected s ⇒ connected (closure s)

⊢ ∀s x.
    connected_component s x = BIGUNION {t | connected t ∧ x ∈ t ∧ t ⊆ s}

⊢ ∀s a b.
    DISJOINT (connected_component s a) (connected_component s b) ⇔
    a ∉ connected_component s b

⊢ ∀x. connected_component ∅ x = ∅

⊢ ∀s x y.
    y ∈ connected_component s x ⇒
    connected_component s y = connected_component s x

⊢ ∀R s.
    (∀x y. R x y ⇒ R y x) ∧ (∀x y z. R x y ∧ R y z ⇒ R x z) ∧
    (∀a. a ∈ s ⇒
         ∃t. open_in (subtopology euclidean s) t ∧ a ∈ t ∧
             ∀x. x ∈ t ⇒ R a x) ⇒
    ∀a b. connected_component s a b ⇒ R a b

⊢ ∀s x. connected_component s x = ∅ ⇔ x ∉ s

⊢ ∀s x y.
    connected_component s x = connected_component s y ⇔
    x ∉ s ∧ y ∉ s ∨ x ∈ s ∧ y ∈ s ∧ connected_component s x y

⊢ ∀s x. connected s ∧ x ∈ s ⇒ connected_component s x = s

⊢ ∀s x. connected_component s x = 𝕌(:real) ⇔ s = 𝕌(:real)

⊢ ∀s x.
    connected_component (connected_component s x) x =
    connected_component s x

⊢ ∀s x y. connected_component s x y ⇒ x ∈ s ∧ y ∈ s

⊢ ∀t u a.
    connected_component u a ⊆ t ∧ t ⊆ u ⇒
    connected_component t a = connected_component u a

⊢ ∀s t x. x ∈ t ∧ connected t ∧ t ⊆ s ⇒ t ⊆ connected_component s x

⊢ ∀s t x. s ⊆ t ⇒ connected_component s x ⊆ connected_component t x

⊢ ∀s a b.
    connected_component s a ∩ connected_component s b = ∅ ⇔
    a ∉ s ∨ b ∉ s ∨ connected_component s a ≠ connected_component s b

⊢ ∀s t x. s ⊆ t ∧ connected_component s x y ⇒ connected_component t x y

⊢ ∀s a b.
    connected_component s a ∩ connected_component s b ≠ ∅ ⇔
    a ∈ s ∧ b ∈ s ∧ connected_component s a = connected_component s b

⊢ ∀s x. x ∈ s ⇒ connected_component s x x

⊢ ∀s x. connected_component s x x ⇔ x ∈ s

⊢ ∀s x.
    connected_component s x = {y | ∃t. connected t ∧ t ⊆ s ∧ x ∈ t ∧ y ∈ t}

⊢ ∀s x. connected_component s x ⊆ s

⊢ ∀s x y. connected_component s x y ⇒ connected_component s y x

⊢ ∀s x y. connected_component s x y ⇔ connected_component s y x

⊢ ∀s x y.
    connected_component s x y ∧ connected_component s y z ⇒
    connected_component s x z

⊢ ∀s c x.
    x ∈ c ∧ c ⊆ s ∧ connected c ∧
    (∀c'. x ∈ c' ∧ c' ⊆ s ∧ connected c' ⇒ c' ⊆ c) ⇒
    connected_component s x = c

⊢ ∀x. connected_component 𝕌(:real) x = 𝕌(:real)

⊢ ∀s x. connected (connected_component s x)

⊢ ∀s. connected s ⇔ ∀x. x ∈ s ⇒ connected_component s x = s

⊢ ∀f s. f continuous_on s ∧ connected s ⇒ connected (IMAGE f s)

⊢ ∀s t u.
    s ⊆ t ∧ t ⊆ u ∧ open s ∧ closed t ∧ connected u ∧ connected (t DIFF s) ⇒
    connected (u DIFF s)

⊢ ∀f f'.
    pairwiseD DISJOINT f ∧ pairwiseD DISJOINT f' ∧
    (∀s. s ∈ f ⇒ open s ∧ connected s ∧ s ≠ ∅) ∧
    (∀s. s ∈ f' ⇒ open s ∧ connected s ∧ s ≠ ∅) ∧ BIGUNION f = BIGUNION f' ⇒
    f = f'

⊢ connected ∅

⊢ ∀R s.
    connected s ∧ (∀x y. R x y ⇒ R y x) ∧ (∀x y z. R x y ∧ R y z ⇒ R x z) ∧
    (∀a. a ∈ s ⇒
         ∃t. open_in (subtopology euclidean s) t ∧ a ∈ t ∧
             ∀x. x ∈ t ⇒ R a x) ⇒
    ∀a b. a ∈ s ∧ b ∈ s ⇒ R a b

⊢ ∀P R s.
    connected s ∧ (∀x y. R x y ⇒ R y x) ∧ (∀x y z. R x y ∧ R y z ⇒ R x z) ∧
    (∀t a. open_in (subtopology euclidean s) t ∧ a ∈ t ⇒ ∃z. z ∈ t ∧ P z) ∧
    (∀a. a ∈ s ⇒
         ∃t. open_in (subtopology euclidean s) t ∧ a ∈ t ∧
             ∀x y. x ∈ t ∧ y ∈ t ∧ P x ∧ P y ⇒ R x y) ⇒
    ∀a b. a ∈ s ∧ b ∈ s ∧ P a ∧ P b ⇒ R a b

⊢ ∀s. connected s ⇔ components s ⊆ {s}

⊢ ∀s. connected s ⇔ ∃a. components s ⊆ {a}

⊢ ∀s. connected s ⇔ ∀c c'. c ∈ components s ∧ c' ∈ components s ⇒ c = c'

⊢ ∀s. connected s ⇔
      ∀x y.
        x ∈ s ∧ y ∈ s ⇒ connected_component s x = connected_component s y

⊢ ∀s t.
    closed s ∧ closed t ∧ connected (s ∪ t) ∧ connected (s ∩ t) ⇒
    connected s ∧ connected t

⊢ ∀s t.
    open s ∧ open t ∧ connected (s ∪ t) ∧ connected (s ∩ t) ⇒
    connected s ∧ connected t

⊢ ∀s. connected s ⇔
      ∀a b. a ∈ s ∧ b ∈ s ⇒ ∃t. connected t ∧ t ⊆ s ∧ a ∈ t ∧ b ∈ t

⊢ ∀s. connected s ⇔ ∀x y. x ∈ s ∧ y ∈ s ⇒ connected_component s x y

⊢ ∀s x. connected s ∧ ¬(∃a. s = {a}) ∧ x ∈ s ⇒ x limit_point_of s

⊢ ∀s x.
    connected s ∧ closed s ∧ ¬(∃a. s = {a}) ⇒ (x limit_point_of s ⇔ x ∈ s)

⊢ ∀P Q s.
    connected s ∧
    (∀t a. open_in (subtopology euclidean s) t ∧ a ∈ t ⇒ ∃z. z ∈ t ∧ P z) ∧
    (∀a. a ∈ s ⇒
         ∃t. open_in (subtopology euclidean s) t ∧ a ∈ t ∧
             ∀x y. x ∈ t ∧ y ∈ t ∧ P x ∧ P y ∧ Q x ⇒ Q y) ⇒
    ∀a b. a ∈ s ∧ b ∈ s ∧ P a ∧ P b ∧ Q a ⇒ Q b

⊢ ∀P s.
    connected s ∧
    (∀a. a ∈ s ⇒
         ∃t. open_in (subtopology euclidean s) t ∧ a ∈ t ∧
             ∀x y. x ∈ t ∧ y ∈ t ∧ P x ⇒ P y) ⇒
    ∀a b. a ∈ s ∧ b ∈ s ∧ P a ⇒ P b

⊢ ∀s t. connected s ∧ s ⊆ t ∧ t ⊆ closure s ⇒ connected t

⊢ ∀a b. connected (interval (a,b)) ∧ connected (interval [(a,b)])

⊢ ∀s t. connected s ∧ s ∩ t ≠ ∅ ∧ s DIFF t ≠ ∅ ⇒ s ∩ frontier t ≠ ∅

⊢ ∀s x y a. connected s ∧ x ∈ s ∧ y ∈ s ∧ x ≤ a ∧ a ≤ y ⇒ a ∈ s

⊢ ∀s x y a. connected s ∧ x ∈ s ∧ y ∈ s ∧ x ≤ a ∧ a ≤ y ⇒ ∃z. z ∈ s ∧ z = a

⊢ ∀s x y a b.
    connected s ∧ x ∈ s ∧ y ∈ s ∧ a * x ≤ b ∧ b ≤ a * y ⇒
    ∃z. z ∈ s ∧ a * z = b

⊢ ∀f s. connected s ∧ linear f ⇒ connected (IMAGE f s)

⊢ ∀f s t.
    f continuous_on s ∧ IMAGE f s = t ∧
    (∀u. u ⊆ t ⇒
         (open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ u} ⇔
          open_in (subtopology euclidean t) u)) ∧
    (∀y. y ∈ t ⇒ connected {x | x ∈ s ∧ f x = y}) ∧ connected t ⇒
    connected s

⊢ ∀f s t c.
    IMAGE f s = t ∧
    (∀u. u ⊆ t ⇒
         (open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ u} ⇔
          open_in (subtopology euclidean t) u)) ∧
    (∀y. y ∈ t ⇒ connected {x | x ∈ s ∧ f x = y}) ∧
    (open_in (subtopology euclidean t) c ∨
     closed_in (subtopology euclidean t) c) ∧ connected c ⇒
    connected {x | x ∈ s ∧ f x ∈ c}

⊢ ∀s. connected s ⇒ connected (IMAGE (λx. -x) s)

⊢ ∀s. (∀n. compact (s n) ∧ connected (s n)) ∧ (∀m n. m ≤ n ⇒ s n ⊆ s m) ⇒
      connected (BIGINTER {s n | n ∈ 𝕌(:num)})

⊢ ∀s. (∀n. closed (s n) ∧ connected (s n)) ∧ (∃n. compact (s n)) ∧
      (∀m n. m ≤ n ⇒ s n ⊆ s m) ⇒
      connected (BIGINTER {s n | n ∈ 𝕌(:num)})

⊢ ∀s. connected s ⇔
      ¬∃e1 e2.
        open_in (subtopology euclidean s) e1 ∧
        open_in (subtopology euclidean s) e2 ∧ s ⊆ e1 ∪ e2 ∧ e1 ∩ e2 = ∅ ∧
        e1 ≠ ∅ ∧ e2 ≠ ∅

⊢ ∀s. connected s ⇔
      ¬∃e1 e2.
        open_in (subtopology euclidean s) e1 ∧
        open_in (subtopology euclidean s) e2 ∧ e1 ∪ e2 = s ∧ e1 ∩ e2 = ∅ ∧
        e1 ≠ ∅ ∧ e2 ≠ ∅

⊢ ∀f s t.
    f continuous_on s ∧ IMAGE f s = t ∧
    (∀c. open_in (subtopology euclidean s) c ⇒
         open_in (subtopology euclidean t) (IMAGE f c)) ∧
    (∀y. y ∈ t ⇒ connected {x | x ∈ s ∧ f x = y}) ⇒
    ∀c. connected c ∧ c ⊆ t ⇒ connected {x | x ∈ s ∧ f x ∈ c}

⊢ ∀s. open s ⇒
      (connected s ⇔
       ¬∃e1 e2.
         open e1 ∧ open e2 ∧ e1 ≠ ∅ ∧ e2 ≠ ∅ ∧ e1 ∪ e2 = s ∧ e1 ∩ e2 = ∅)

⊢ ∀f a b e1 e2.
    a ≤ b ∧ f a ∈ e1 ∧ f b ∈ e2 ∧
    (∀e x.
       a ≤ x ∧ x ≤ b ∧ 0 < e ⇒
       ∃d. 0 < d ∧ ∀y. abs (y − x) < d ⇒ dist (f y,f x) < e) ∧
    (∀y. y ∈ e1 ⇒ ∃e. 0 < e ∧ ∀y'. dist (y',y) < e ⇒ y' ∈ e1) ∧
    (∀y. y ∈ e2 ⇒ ∃e. 0 < e ∧ ∀y'. dist (y',y) < e ⇒ y' ∈ e2) ∧
    ¬(∃x. a ≤ x ∧ x ≤ b ∧ f x ∈ e1 ∧ f x ∈ e2) ⇒
    ∃x. a ≤ x ∧ x ≤ b ∧ f x ∉ e1 ∧ f x ∉ e2

⊢ ∀s c. connected s ⇒ connected (IMAGE (λx. c * x) s)

⊢ (∀a b. connected (segment [(a,b)])) ∧ ∀a b. connected (segment (a,b))

⊢ ∀a. connected {a}

⊢ ∀u s c.
    closed_in (subtopology euclidean u) s ∧
    open_in (subtopology euclidean u) s ∧ connected c ∧ c ⊆ u ∧ c ∩ s ≠ ∅ ⇒
    c ⊆ s

⊢ ∀a s. connected s ⇒ connected (IMAGE (λx. a + x) s)

⊢ ∀a s. connected (IMAGE (λx. a + x) s) ⇔ connected s

⊢ ∀s t. connected s ∧ connected t ∧ s ∩ t ≠ ∅ ⇒ connected (s ∪ t)

⊢ ∀s t. connected s ∧ connected t ∧ closure s ∩ t ≠ ∅ ⇒ connected (s ∪ t)

⊢ connected 𝕌(:real)

⊢ ∀s a b.
    s ⊆ interval [(a,b)] ∧ content (interval [(a,b)]) = 0 ⇒ content s = 0

⊢ ∀s t. s ⊆ t ∧ bounded t ∧ content t = 0 ⇒ content s = 0

⊢ ∀a b. a ≤ b ⇒ content (interval [(a,b)]) = b − a

⊢ ∀a b. content (interval [(a,b)]) = if a ≤ b then b − a else 0

⊢ content ∅ = 0

⊢ ∀a b. content (interval [(a,b)]) = 0 ⇔ b ≤ a

⊢ ∀a b. content (interval [(a,b)]) = 0 ⇔ b ≤ a

⊢ ∀s. bounded s ⇒ (content s = 0 ⇔ ∃a. ∀x. x ∈ s ⇒ x = a)

⊢ ∀a b. content (interval [(a,b)]) = 0 ⇔ interior (interval [(a,b)]) = ∅

⊢ ∀a b. 0 < content (interval [(a,b)]) ⇔ content (interval [(a,b)]) ≠ 0

⊢ ∀a b. 0 ≤ content (interval [(a,b)])

⊢ ∀a b. a < b ⇒ 0 < content (interval [(a,b)])

⊢ ∀a b. 0 < content (interval [(a,b)]) ⇔ a < b

⊢ ∀a b c d.
    interval [(a,b)] ⊆ interval [(c,d)] ⇒
    content (interval [(a,b)]) ≤ content (interval [(c,d)])

⊢ content (interval [(0,1)]) = 1

⊢ ∀f net. f continuous net ⇒ (λx. abs (f x)) continuous net

⊢ ∀net f. f continuous net ⇒ (λx. abs (f x)) continuous net

⊢ ∀f g net.
    f continuous net ∧ g continuous net ⇒ (λx. f x + g x) continuous net

⊢ ∀g h.
    g continuous_on closure s ∧ h continuous_on closure s ∧
    (∀x. x ∈ s ⇒ g x = h x) ⇒
    ∀x. x ∈ closure s ⇒ g x = h x

⊢ ∀f x. f continuous at x ⇔ (f ⟶ f x) (at x)

⊢ ∀f s.
    compact s ∧ s ≠ ∅ ∧ f continuous_on s ⇒
    ∃x. x ∈ s ∧ ∀y. y ∈ s ⇒ f x ≤ f y

⊢ ∀f s.
    compact s ∧ s ≠ ∅ ∧ f continuous_on s ⇒
    ∃x. x ∈ s ∧ ∀y. y ∈ s ⇒ f y ≤ f x

⊢ ∀x. abs continuous at x

⊢ ∀f x a.
    f continuous at x ∧ f x ≠ a ⇒ ∃e. 0 < e ∧ ∀y. dist (x,y) < e ⇒ f y ≠ a

⊢ ∀f x.
    f continuous at x ⇔
    ∀e. 0 < e ⇒ ∃d. 0 < d ∧ IMAGE f (ball (x,d)) ⊆ ball (f x,e)

⊢ ∀f g x. f continuous at x ∧ g continuous at (f x) ⇒ g ∘ f continuous at x

⊢ ∀f g h.
    g continuous at x ∧ h continuous at (g x) ∧ (∀y. g (h y) = y) ∧
    h (g x) = x ⇒
    (f continuous at (g x) ⇔ (λx. f (g x)) continuous at x)

⊢ ∀a x. (λx. dist (a,x)) continuous at x

⊢ ∀s x. closed s ∧ s ≠ ∅ ⇒ (λx. dist (x,closest_point s x)) continuous at x

⊢ ∀a. (λx. x) continuous at a

⊢ ∀f s. (∀x. x ∈ s ⇒ f continuous at x) ⇒ f continuous_on s

⊢ ∀f a. f continuous at a ∧ f a ≠ 0 ⇒ realinv ∘ f continuous at a

⊢ ∀a x. (λy. a * y) continuous at x

⊢ ∀f x.
    f continuous at x ⇔
    ∀t. open t ∧ f x ∈ t ⇒ ∃s. open s ∧ x ∈ s ∧ ∀x'. x' ∈ s ⇒ f x' ∈ t

⊢ ∀f x.
    f continuous at x ⇔
    ∀e. 0 < e ⇒ ∃d. 0 < d ∧ ∀x'. abs (x' − x) < d ⇒ abs (f x' − f x) < e

⊢ ∀f a.
    f continuous at a ⇔
    ∀x. (x ⟶ a) sequentially ⇒ (f ∘ x ⟶ f a) sequentially

⊢ ∀s x. (λy. setdist ({y},s)) continuous at x

⊢ ∀a z f. f continuous at (a + z) ⇔ (λx. f (a + x)) continuous at z

⊢ ∀f x s. f continuous at x ⇒ f continuous (at x within s)

⊢ ∀f s a.
    f continuous (at a within s) ∧ f a ≠ 0 ⇒
    realinv ∘ f continuous (at a within s)

⊢ ∀f s.
    f continuous_on s ∧ closed s ⇒
    ∀x. cauchy x ∧ (∀n. x n ∈ s) ⇒ cauchy (f ∘ x)

⊢ ∀f s t.
    f continuous_on s ∧ closed t ⇒
    closed_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ t}

⊢ ∀f s a.
    f continuous_on s ⇒
    closed_in (subtopology euclidean s) {x | x ∈ s ∧ f x = a}

⊢ ∀f s.
    f continuous_on s ⇔
    ∀t. closed t ⇒
        closed_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ t}

⊢ ∀f s t u.
    f continuous_on s ∧ IMAGE f s ⊆ t ∧
    closed_in (subtopology euclidean t) u ⇒
    closed_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ u}

⊢ ∀f s t.
    f continuous_on s ∧ closed s ∧ closed t ⇒ closed {x | x ∈ s ∧ f x ∈ t}

⊢ ∀f s. f continuous_on s ∧ closed s ⇒ closed {x | x ∈ s ∧ f x = a}

⊢ ∀f s. (∀x. f continuous at x) ∧ closed s ⇒ closed {x | f x ∈ s}

⊢ ∀f c net. f continuous net ⇒ (λx. c * f x) continuous net

⊢ ∀net f i. f continuous net ⇒ (λx. f x) continuous net

⊢ ∀net c. (λx. c) continuous net

⊢ ∀f s a.
    f continuous_on closure s ∧ (∀x. x ∈ s ⇒ f x = a) ⇒
    ∀x. x ∈ closure s ⇒ f x = a

⊢ ∀s e.
    bounded s ∧ s ≠ ∅ ∧ 0 < e ⇒
    ∃d. 0 < d ∧
        ∀t. bounded t ∧ t ≠ ∅ ∧ hausdist (s,t) < d ⇒
            abs (diameter s − diameter t) < e

⊢ (∀s. connected s ⇔
       ∀f t.
         f continuous_on s ∧ IMAGE f s ⊆ t ∧
         (∀y. y ∈ t ⇒ connected_component t y = {y}) ⇒
         ∃a. ∀x. x ∈ s ⇒ f x = a) ∧
  (∀s. connected s ⇔
       ∀f. f continuous_on s ∧
           (∀x. x ∈ s ⇒
                ∃e. 0 < e ∧ ∀y. y ∈ s ∧ f y ≠ f x ⇒ e ≤ abs (f y − f x)) ⇒
           ∃a. ∀x. x ∈ s ⇒ f x = a) ∧
  ∀s. connected s ⇔
      ∀f. f continuous_on s ∧ FINITE (IMAGE f s) ⇒ ∃a. ∀x. x ∈ s ⇒ f x = a

⊢ ∀f s.
    connected s ∧ f continuous_on s ∧ IMAGE f s ⊆ t ∧
    (∀y. y ∈ t ⇒ connected_component t y = {y}) ⇒
    ∃a. ∀x. x ∈ s ⇒ f x = a

⊢ ∀s. connected s ⇔
      ∀f t.
        f continuous_on s ∧ IMAGE f s ⊆ t ∧
        (∀y. y ∈ t ⇒ connected_component t y = {y}) ⇒
        ∃a. ∀x. x ∈ s ⇒ f x = a

⊢ ∀f s.
    connected s ∧ f continuous_on s ∧
    (∀x. x ∈ s ⇒ ∃e. 0 < e ∧ ∀y. y ∈ s ∧ f y ≠ f x ⇒ e ≤ abs (f y − f x)) ⇒
    ∃a. ∀x. x ∈ s ⇒ f x = a

⊢ ∀s. connected s ⇔
      ∀f. f continuous_on s ∧
          (∀x. x ∈ s ⇒
               ∃e. 0 < e ∧ ∀y. y ∈ s ∧ f y ≠ f x ⇒ e ≤ abs (f y − f x)) ⇒
          ∃a. ∀x. x ∈ s ⇒ f x = a

⊢ ∀net f g.
    f continuous net ∧ g continuous net ⇒ (λx. f x * g x) continuous net

⊢ ∀f s.
    connected s ∧ f continuous_on s ∧ FINITE (IMAGE f s) ⇒
    ∃a. ∀x. x ∈ s ⇒ f x = a

⊢ ∀s. connected s ⇔
      ∀f. f continuous_on s ∧ FINITE (IMAGE f s) ⇒ ∃a. ∀x. x ∈ s ⇒ f x = a

⊢ ∀f s a.
    f continuous_on closure s ∧ (∀x. x ∈ s ⇒ a ≤ f x) ⇒
    ∀x. x ∈ closure s ⇒ a ≤ f x

⊢ ∀f s t.
    f continuous_on s ∧ IMAGE f s = t ∧ compact s ⇒
    ∀u. closed_in (subtopology euclidean s) u ⇒
        closed_in (subtopology euclidean t) (IMAGE f u)

⊢ ∀f s t.
    f continuous_on s ∧ IMAGE f s = t ∧ compact s ⇒
    ∀u. u ⊆ t ⇒
        (open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ u} ⇔
         open_in (subtopology euclidean t) u)

⊢ ∀net f.
    f continuous net ∧ f (netlimit net) ≠ 0 ⇒ realinv ∘ f continuous net

⊢ ∀f g s.
    f continuous_on s ∧ g continuous_on IMAGE f s ∧
    (∀x. x ∈ s ⇒ g (f x) = x) ⇒
    ∀u. u ⊆ IMAGE f s ⇒
        (open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ u} ⇔
         open_in (subtopology euclidean (IMAGE f s)) u)

⊢ ∀f s a.
    connected s ∧ f continuous_on s ∧ open {x | x ∈ s ∧ f x = a} ∧
    (∃x. x ∈ s ∧ f x = a) ⇒
    ∀x. x ∈ s ⇒ f x = a

⊢ ∀f s a.
    connected s ∧ f continuous_on s ∧
    open_in (subtopology euclidean s) {x | x ∈ s ∧ f x = a} ∧
    (∃x. x ∈ s ∧ f x = a) ⇒
    ∀x. x ∈ s ⇒ f x = a

⊢ ∀f s a.
    connected s ∧ f continuous_on s ∧
    open_in (subtopology euclidean s) {x | x ∈ s ∧ f x = a} ⇒
    (∀x. x ∈ s ⇒ f x ≠ a) ∨ ∀x. x ∈ s ⇒ f x = a

⊢ ∀f s a.
    f continuous_on closure s ∧ (∀x. x ∈ s ⇒ f x ≤ a) ⇒
    ∀x. x ∈ closure s ⇒ f x ≤ a

⊢ ∀f. f continuous_on 𝕌(:real) ⇔
      ∀s. IMAGE f (closure s) ⊆ closure (IMAGE f s)

⊢ ∀f g net.
    f continuous net ∧ g continuous net ⇒
    (λx. max (f x) (g x)) continuous net

⊢ ∀f g net.
    f continuous net ∧ g continuous net ⇒
    (λx. min (f x) (g x)) continuous net

⊢ ∀net f c.
    c continuous net ∧ f continuous net ⇒ (λx. c x * f x) continuous net

⊢ ∀f net. f continuous net ⇒ (λx. -f x) continuous net

⊢ ∀f s. f continuous_on s ⇔ ∀x. x ∈ s ⇒ (f ⟶ f x) (at x within s)

⊢ ∀f s. f continuous_on s ⇒ (λx. abs (f x)) continuous_on s

⊢ ∀f s. f continuous_on s ⇒ (λx. abs (f x)) continuous_on s

⊢ ∀f g s.
    f continuous_on s ∧ g continuous_on s ⇒ (λx. f x + g x) continuous_on s

⊢ ∀f x s a.
    f continuous_on s ∧ x ∈ s ∧ f x ≠ a ⇒
    ∃e. 0 < e ∧ ∀y. y ∈ s ∧ dist (x,y) < e ⇒ f y ≠ a

⊢ ∀P f g s t.
    closed s ∧ closed t ∧ f continuous_on s ∧ g continuous_on t ∧
    (∀x. x ∈ s ∧ ¬P x ∨ x ∈ t ∧ P x ⇒ f x = g x) ⇒
    (λx. if P x then f x else g x) continuous_on s ∪ t

⊢ ∀f g s a.
    f continuous_on {t | t ∈ s ∧ t ≤ a} ∧
    g continuous_on equiv_class $<= s a ∧ (a ∈ s ⇒ f a = g a) ⇒
    (λt. if t ≤ a then f t else g t) continuous_on s

⊢ ∀f g h s a.
    f continuous_on {t | t ∈ s ∧ h t ≤ a} ∧
    g continuous_on {t | t ∈ s ∧ a ≤ h t} ∧ h continuous_on s ∧
    (∀t. t ∈ s ∧ h t = a ⇒ f t = g t) ⇒
    (λt. if h t ≤ a then f t else g t) continuous_on s

⊢ ∀P f g s t.
    closed_in (subtopology euclidean (s ∪ t)) s ∧
    closed_in (subtopology euclidean (s ∪ t)) t ∧ f continuous_on s ∧
    g continuous_on t ∧ (∀x. x ∈ s ∧ ¬P x ∨ x ∈ t ∧ P x ⇒ f x = g x) ⇒
    (λx. if P x then f x else g x) continuous_on s ∪ t

⊢ ∀P f g s t.
    open_in (subtopology euclidean (s ∪ t)) s ∧
    open_in (subtopology euclidean (s ∪ t)) t ∧ f continuous_on s ∧
    g continuous_on t ∧ (∀x. x ∈ s ∧ ¬P x ∨ x ∈ t ∧ P x ⇒ f x = g x) ⇒
    (λx. if P x then f x else g x) continuous_on s ∪ t

⊢ ∀P f g s t.
    open s ∧ open t ∧ f continuous_on s ∧ g continuous_on t ∧
    (∀x. x ∈ s ∧ ¬P x ∨ x ∈ t ∧ P x ⇒ f x = g x) ⇒
    (λx. if P x then f x else g x) continuous_on s ∪ t

⊢ ∀f s.
    f continuous_on s ⇔
    ∀t. closed_in (subtopology euclidean (IMAGE f s)) t ⇒
        closed_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ t}

⊢ ∀f s t.
    IMAGE f s ⊆ t ⇒
    (f continuous_on s ⇔
     ∀u. closed_in (subtopology euclidean t) u ⇒
         closed_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ u})

⊢ ∀f s.
    f continuous_on closure s ⇔
    ∀x e.
      x ∈ closure s ∧ 0 < e ⇒
      ∃d. 0 < d ∧ ∀y. y ∈ s ∧ dist (y,x) < d ⇒ dist (f y,f x) < e

⊢ ∀f s x b.
    f continuous_on closure s ∧ (∀y. y ∈ s ⇒ abs (f y) ≤ b) ∧ x ∈ closure s ⇒
    abs (f x) ≤ b

⊢ ∀f s x b.
    f continuous_on closure s ∧ (∀y. y ∈ s ⇒ b ≤ f y) ∧ x ∈ closure s ⇒
    b ≤ f x

⊢ ∀f s x b.
    f continuous_on closure s ∧ (∀y. y ∈ s ⇒ f y ≤ b) ∧ x ∈ closure s ⇒
    f x ≤ b

⊢ ∀f s.
    f continuous_on closure s ⇔
    ∀x a.
      a ∈ closure s ∧ (∀n. x n ∈ s) ∧ (x ⟶ a) sequentially ⇒
      (f ∘ x ⟶ f a) sequentially

⊢ ∀f c s. f continuous_on s ⇒ (λx. c * f x) continuous_on s

⊢ ∀f s.
    FINITE (components s) ∧ (∀c. c ∈ components s ⇒ f continuous_on c) ⇒
    f continuous_on s

⊢ ∀f s.
    (∀c. c ∈ components s ⇒
         open_in (subtopology euclidean s) c ∧ f continuous_on c) ⇒
    f continuous_on s

⊢ ∀f s. f continuous_on s ⇒ (λx. f x) continuous_on s

⊢ ∀f g s.
    f continuous_on s ∧ g continuous_on IMAGE f s ⇒ g ∘ f continuous_on s

⊢ ∀f g s t u.
    IMAGE f s ⊆ t ∧ IMAGE g t ⊆ u ∧
    (∀v. v ⊆ t ⇒
         (open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ v} ⇔
          open_in (subtopology euclidean t) v)) ∧ g ∘ f continuous_on s ⇒
    g continuous_on t

⊢ ∀s c. (λx. c) continuous_on s

⊢ ∀a s. (λx. dist (a,x)) continuous_on s

⊢ ∀s t. closed s ∧ s ≠ ∅ ⇒ (λx. dist (x,closest_point s x)) continuous_on t

⊢ ∀f g s.
    f continuous_on s ∧ g continuous_on s ⇒ (λx. f x * g x) continuous_on s

⊢ ∀f. f continuous_on ∅

⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ∧ f continuous_on s ⇒ g continuous_on s

⊢ ∀f s. open s ⇒ (f continuous_on s ⇔ ∀x. x ∈ s ⇒ f continuous at x)

⊢ ∀f s. f continuous_on s ⇔ ∀x. x ∈ s ⇒ f continuous (at x within s)

⊢ ∀f s. FINITE s ⇒ f continuous_on s

⊢ ∀s. (λx. x) continuous_on s

⊢ ∀f s t.
    f continuous_on s ∧ closed_in (subtopology euclidean (IMAGE f s)) t ⇒
    closed_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ t}

⊢ ∀f s t.
    f continuous_on s ∧ open_in (subtopology euclidean (IMAGE f s)) t ⇒
    open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ t}

⊢ ∀f s x. f continuous_on s ∧ x ∈ interior s ⇒ f continuous at x

⊢ ∀f s.
    f continuous_on s ∧ (∀x. x ∈ s ⇒ f x ≠ 0) ⇒ realinv ∘ f continuous_on s

⊢ ∀f g s.
    f continuous_on s ∧ compact s ∧ (∀x. x ∈ s ⇒ g (f x) = x) ⇒
    g continuous_on IMAGE f s

⊢ ∀f g s t.
    f continuous_on s ∧ IMAGE f s = t ∧ (∀x. x ∈ s ⇒ g (f x) = x) ∧
    (∀u. closed_in (subtopology euclidean s) u ⇒
         closed_in (subtopology euclidean t) (IMAGE f u)) ⇒
    g continuous_on t

⊢ ∀f g s t.
    f continuous_on s ∧ IMAGE f s = t ∧ (∀x. x ∈ s ⇒ g (f x) = x) ∧
    (∀u. open_in (subtopology euclidean s) u ⇒
         open_in (subtopology euclidean t) (IMAGE f u)) ⇒
    g continuous_on t

⊢ ∀f a b y.
    a ≤ b ∧ f a ≤ y ∧ y ≤ f b ∧ f continuous_on interval [(a,b)] ⇒
    ∃x. x ∈ interval [(a,b)] ∧ f x = y

⊢ ∀s. (λy. a * y) continuous_on s

⊢ ∀f g s.
    f continuous_on s ∧ g continuous_on s ⇒
    (λx. max (f x) (g x)) continuous_on s

⊢ ∀f g s.
    f continuous_on s ∧ g continuous_on s ⇒
    (λx. min (f x) (g x)) continuous_on s

⊢ ∀s c f.
    c continuous_on s ∧ f continuous_on s ⇒ (λx. c x * f x) continuous_on s

⊢ ∀f s. f continuous_on s ⇒ (λx. -f x) continuous_on s

⊢ ∀f s. ¬(∃x. x limit_point_of s) ⇒ f continuous_on s

⊢ ∀f s.
    f continuous_on s ⇔
    ∀t. open_in (subtopology euclidean (IMAGE f s)) t ⇒
        open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ t}

⊢ ∀f x s a.
    f continuous_on s ∧ open s ∧ x ∈ s ∧ f x ≠ a ⇒
    ∃e. 0 < e ∧ ∀y. dist (x,y) < e ⇒ f y ≠ a

⊢ ∀f s t.
    IMAGE f s ⊆ t ⇒
    (f continuous_on s ⇔
     ∀u. open_in (subtopology euclidean t) u ⇒
         open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ u})

⊢ ∀f s n. (λx. f x) continuous_on s ⇒ (λx. f x pow n) continuous_on s

⊢ ∀f s t.
    FINITE t ∧ (∀i. i ∈ t ⇒ (λx. f x i) continuous_on s) ⇒
    (λx. product t (f x)) continuous_on s

⊢ ∀f s.
    f continuous_on s ⇔
    ∀x. x ∈ s ⇒
        ∀e. 0 < e ⇒
            ∃d. 0 < d ∧
                ∀x'. x' ∈ s ∧ abs (x' − x) < d ⇒ abs (f x' − f x) < e

⊢ ∀f s.
    f continuous_on s ⇔
    ∀x a.
      a ∈ s ∧ (∀n. x n ∈ s) ∧ (x ⟶ a) sequentially ⇒
      (f ∘ x ⟶ f a) sequentially

⊢ ∀s t. (λy. setdist ({y},s)) continuous_on t

⊢ ∀f a. f continuous_on {a}

⊢ ∀f g s.
    f continuous_on s ∧ g continuous_on s ⇒ (λx. f x − g x) continuous_on s

⊢ ∀f s t. f continuous_on s ∧ t ⊆ s ⇒ f continuous_on t

⊢ ∀t f s.
    FINITE s ∧ (∀a. a ∈ s ⇒ f a continuous_on t) ⇒
    (λx. sum s (λa. f a x)) continuous_on t

⊢ ∀f s t.
    closed s ∧ closed t ∧ f continuous_on s ∧ f continuous_on t ⇒
    f continuous_on s ∪ t

⊢ ∀f s.
    closed_in (subtopology euclidean (s ∪ t)) s ∧
    closed_in (subtopology euclidean (s ∪ t)) t ∧ f continuous_on s ∧
    f continuous_on t ⇒
    f continuous_on s ∪ t

⊢ ∀f s.
    open_in (subtopology euclidean (s ∪ t)) s ∧
    open_in (subtopology euclidean (s ∪ t)) t ∧ f continuous_on s ∧
    f continuous_on t ⇒
    f continuous_on s ∪ t

⊢ ∀f s t.
    open s ∧ open t ∧ f continuous_on s ∧ f continuous_on t ⇒
    f continuous_on s ∪ t

⊢ ∀s c v. c continuous_on s ⇒ (λx. c x * v) continuous_on s

⊢ ∀f s t.
    f continuous_on s ∧ open t ⇒
    open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ t}

⊢ ∀f s.
    f continuous_on s ⇔
    ∀t. open t ⇒ open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ t}

⊢ ∀f s t u.
    f continuous_on s ∧ IMAGE f s ⊆ t ∧ open_in (subtopology euclidean t) u ⇒
    open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ u}

⊢ ∀f s t. f continuous_on s ∧ open s ∧ open t ⇒ open {x | x ∈ s ∧ f x ∈ t}

⊢ ∀f s. (∀x. f continuous at x) ∧ open s ⇒ open {x | f x ∈ s}

⊢ ∀net f n. (λx. f x) continuous net ⇒ (λx. f x pow n) continuous net

⊢ ∀net f t.
    FINITE t ∧ (∀i. i ∈ t ⇒ (λx. f x i) continuous net) ⇒
    (λx. product t (f x)) continuous net

⊢ ∀f g s t.
    f continuous_on s ∧ IMAGE f s ⊆ t ∧ g continuous_on t ∧ IMAGE g t ⊆ s ∧
    (∀y. y ∈ t ⇒ f (g y) = y) ⇒
    ∀u. u ⊆ t ⇒
        (open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ u} ⇔
         open_in (subtopology euclidean t) u)

⊢ ∀f g net.
    f continuous net ∧ g continuous net ⇒ (λx. f x − g x) continuous net

⊢ ∀net f s.
    FINITE s ∧ (∀a. a ∈ s ⇒ f a continuous net) ⇒
    (λx. sum s (λa. f a x)) continuous net

⊢ ∀f g x d.
    0 < d ∧ (∀x'. dist (x',x) < d ⇒ f x' = g x') ∧ f continuous at x ⇒
    g continuous at x

⊢ ∀f g s x d.
    0 < d ∧ x ∈ s ∧ (∀x'. x' ∈ s ∧ dist (x',x) < d ⇒ f x' = g x') ∧
    f continuous (at x within s) ⇒
    g continuous (at x within s)

⊢ ∀f g s a.
    open s ∧ a ∈ s ∧ (∀x. x ∈ s ⇒ f x = g x) ∧ f continuous at a ⇒
    g continuous at a

⊢ ∀f g s t a.
    open_in (subtopology euclidean t) s ∧ a ∈ s ∧ (∀x. x ∈ s ⇒ f x = g x) ∧
    f continuous (at a within t) ⇒
    g continuous (at a within t)

⊢ ∀f a s t.
    eventually (λx. x ∈ t ⇒ x ∈ s) (at a) ∧ f continuous (at a within s) ⇒
    f continuous (at a within t)

⊢ ∀f net. trivial_limit net ⇒ f continuous net

⊢ ∀net f g s.
    ¬trivial_limit net ∧ eventually (λn. f n continuous_on s) net ∧
    (∀e. 0 < e ⇒ eventually (λn. ∀x. x ∈ s ⇒ abs (f n x − g x) < e) net) ⇒
    g continuous_on s

⊢ ∀net c v. c continuous net ⇒ (λx. c x * v) continuous net

⊢ ∀f x. f continuous (at x within s) ⇔ (f ⟶ f x) (at x within s)

⊢ ∀f x s a.
    f continuous (at x within s) ∧ x ∈ s ∧ f x ≠ a ⇒
    ∃e. 0 < e ∧ ∀y. y ∈ s ∧ dist (x,y) < e ⇒ f y ≠ a

⊢ ∀f s x.
    f continuous (at x within s) ⇔
    ∀e. 0 < e ⇒ ∃d. 0 < d ∧ IMAGE f (ball (x,d) ∩ s) ⊆ ball (f x,e)

⊢ ∀a s. closed s ∧ a ∉ s ⇒ f continuous (at a within s)

⊢ ∀f g s a.
    g continuous (at a within s) ∧
    (∀x. x ∈ s ⇒ dist (f a,f x) ≤ dist (g a,g x)) ⇒
    f continuous (at a within s)

⊢ ∀f g x s.
    f continuous (at x within s) ∧ g continuous (at (f x) within IMAGE f s) ⇒
    g ∘ f continuous (at x within s)

⊢ ∀a s. (λx. x) continuous (at a within s)

⊢ ∀f x u.
    f continuous (at x within u) ⇔
    ∀t. open t ∧ f x ∈ t ⇒
        ∃s. open s ∧ x ∈ s ∧ ∀x'. x' ∈ s ∧ x' ∈ u ⇒ f x' ∈ t

⊢ ∀f s a.
    f continuous (at a within s) ⇔
    ∀x. (∀n. x n ∈ s) ∧ (x ⟶ a) sequentially ⇒ (f ∘ x ⟶ f a) sequentially

⊢ ∀f s t x.
    f continuous (at x within s) ∧ t ⊆ s ⇒ f continuous (at x within t)

⊢ ∀f. (∀x y. x ∈ s ∧ y ∈ s ⇒ dist (f x,f y) ≤ dist (x,y)) ⇒
      f continuous_on s

⊢ ∀s b.
    (∀m n. m ≤ n ⇒ s m ≤ s n) ∧ (∀n. abs (s n) ≤ b) ⇒
    ∃l. ∀e. 0 < e ⇒ ∃N. ∀n. N ≤ n ⇒ abs (s n − l) < e

⊢ ∀s b.
    (∀n. abs (s n) ≤ b) ∧
    ((∀m n. m ≤ n ⇒ s m ≤ s n) ∨ ∀m n. m ≤ n ⇒ s n ≤ s m) ⇒
    ∃l. ∀e. 0 < e ⇒ ∃N. ∀n. N ≤ n ⇒ abs (s n − l) < e

⊢ ∀s. (∃l. (s ⟶ l) sequentially) ⇔ cauchy s

⊢ ∀s l. (s ⟶ l) sequentially ⇒ bounded (IMAGE s 𝕌(:num))

⊢ ∀s l. (s ⟶ l) sequentially ⇒ cauchy s

⊢ ∀a b. countable (interval (a,b)) ⇔ interval (a,b) = ∅

⊢ ∀s. (∀n. closed (s n)) ∧ (∀n. s n ≠ ∅) ∧ (∀m n. m ≤ n ⇒ s n ⊆ s m) ∧
      (∀e. 0 < e ⇒ ∃n. ∀x y. x ∈ s n ∧ y ∈ s n ⇒ dist (x,y) < e) ⇒
      ∃a. ∀n. a ∈ s n

⊢ ∀s. (∀n. closed (s n)) ∧ (∀n. s n ≠ ∅) ∧ (∀m n. m ≤ n ⇒ s n ⊆ s m) ∧
      (∀e. 0 < e ⇒ ∃n. ∀x y. x ∈ s n ∧ y ∈ s n ⇒ dist (x,y) < e) ⇒
      ∃a. BIGINTER {t | (∃n. t = s n)} = {a}

⊢ ∀s. closure s = 𝕌(:real) ⇒ ∀x. x ∈ s ⇒ x limit_point_of s

⊢ ∀x. {x | x limit_point_of s} = 𝕌(:real) ⇔ closure s = 𝕌(:real)

⊢ ∀s t u.
    open_in (subtopology euclidean u) s ∧ t ⊆ u ∨
    open_in (subtopology euclidean u) t ∧ s ⊆ u ⇒
    (u ⊆ closure (s ∩ t) ⇔ u ⊆ closure s ∧ u ⊆ closure t)

⊢ ∀P R.
    (∃a. P 0 a) ∧ (∀n x. P n x ⇒ ∃y. P (SUC n) y ∧ R n x y) ⇒
    ∃f. (∀n. P n (f n)) ∧ ∀n. R n (f n) (f (SUC n))

⊢ ∀P R a.
    P 0 a ∧ (∀n x. P n x ⇒ ∃y. P (SUC n) y ∧ R n x y) ⇒
    ∃f. f 0 = a ∧ (∀n. P n (f n)) ∧ ∀n. R n (f n) (f (SUC n))

⊢ ∀p. dependent p ⇔
      ∃s u.
        FINITE s ∧ s ⊆ p ∧ (∃v. v ∈ s ∧ u v ≠ 0) ∧ sum s (λv. u v * v) = 0

⊢ ∀s t. dependent s ∧ s ⊆ t ⇒ dependent t

⊢ ∀a r. diameter (ball (a,r)) = if r < 0 then 0 else 2 * r

⊢ ∀s. bounded s ⇒
      (∀x y. x ∈ s ∧ y ∈ s ⇒ abs (x − y) ≤ diameter s) ∧
      ∀d. 0 ≤ d ∧ d < diameter s ⇒ ∃x y. x ∈ s ∧ y ∈ s ∧ abs (x − y) > d

⊢ ∀s x y. bounded s ∧ x ∈ s ∧ y ∈ s ⇒ abs (x − y) ≤ diameter s

⊢ ∀a r. diameter (cball (a,r)) = if r < 0 then 0 else 2 * r

⊢ ∀s. bounded s ⇒ diameter (closure s) = diameter s

⊢ diameter ∅ = 0

⊢ ∀s. bounded s ⇒ (diameter s = 0 ⇔ s = ∅ ∨ ∃a. s = {a})

⊢ (∀a b.
     diameter (interval [(a,b)]) =
     if interval [(a,b)] = ∅ then 0 else abs (b − a)) ∧
  ∀a b.
    diameter (interval (a,b)) =
    if interval (a,b) = ∅ then 0 else abs (b − a)

⊢ ∀s d.
    (s ≠ ∅ ∨ 0 ≤ d) ∧ (∀x y. x ∈ s ∧ y ∈ s ⇒ abs (x − y) ≤ d) ⇒
    diameter s ≤ d

⊢ ∀f s.
    linear f ∧ (∀x. abs (f x) = abs x) ⇒ diameter (IMAGE f s) = diameter s

⊢ ∀s. bounded s ⇒ 0 ≤ diameter s

⊢ ∀a. diameter {a} = 0

⊢ ∀s t. s ⊆ t ∧ bounded t ⇒ diameter s ≤ diameter t

⊢ ∀s. bounded s ⇒ ∃z. s ⊆ cball (z,diameter s)

⊢ ∀s. bounded s ∧ s ≠ ∅ ⇒ ∃z. z ∈ s ∧ s ⊆ cball (z,diameter s)

⊢ ∀s t.
    bounded s ∧ bounded t ⇒
    diameter {x + y | x ∈ s ∧ y ∈ t} ≤ diameter s + diameter t

⊢ ∀s t. closure s DIFF closure t ⊆ closure (s DIFF t)

⊢ ∀s. FINITE s ⇒ dim s ≤ CARD s

⊢ ∀s t. s ⊆ t ⇒ dim s ≤ dim t

⊢ ∀s. dim s ≤ 1

⊢ dim {x | x = 0} = 0

⊢ ∀v b. b ⊆ v ∧ v ⊆ span b ∧ independent b ∧ b HAS_SIZE n ⇒ dim v = n

⊢ dim 𝕌(:real) = 1

⊢ ∀f g s.
    compact s ∧ (∀n. f n continuous_on s) ∧ g continuous_on s ∧
    (∀x. x ∈ s ⇒ ((λn. f n x) ⟶ g x) sequentially) ∧
    (∀n x. x ∈ s ⇒ f n x ≤ f (n + 1) x) ⇒
    ∀e. 0 < e ⇒
        eventually (λn. ∀x. x ∈ s ⇒ abs (f n x − g x) < e) sequentially

⊢ ∀s e.
    0 < e ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ abs (y − x) < e ⇒ y = x) ∧ bounded s ⇒
    FINITE s

⊢ ∀s e. 0 < e ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ abs (y − x) < e ⇒ y = x) ⇒ closed s

⊢ ∀a b c d.
    (interval [(a,b)] ∩ interval [(c,d)] = ∅ ⇔
     b < a ∨ d < c ∨ b < c ∨ d < a) ∧
    (interval [(a,b)] ∩ interval (c,d) = ∅ ⇔ b < a ∨ d ≤ c ∨ b ≤ c ∨ d ≤ a) ∧
    (interval (a,b) ∩ interval [(c,d)] = ∅ ⇔ b ≤ a ∨ d < c ∨ b ≤ c ∨ d ≤ a) ∧
    (interval (a,b) ∩ interval (c,d) = ∅ ⇔ b ≤ a ∨ d ≤ c ∨ b ≤ c ∨ d ≤ a)

⊢ ∀s a. closed s ∧ s ≠ ∅ ⇒ ∃x. x ∈ s ∧ ∀y. y ∈ s ⇒ dist (a,x) ≤ dist (a,y)

⊢ ∀s a. compact s ∧ s ≠ ∅ ⇒ ∃x. x ∈ s ∧ ∀y. y ∈ s ⇒ dist (a,y) ≤ dist (a,x)

⊢ ∀s x y.
    closed s ∧ s ≠ ∅ ⇒
    abs (dist (x,closest_point s x) − dist (y,closest_point s y)) ≤
    dist (x,y)

⊢ ∀a b x.
    x ∈ segment [(a,b)] ⇒ dist (x,a) ≤ dist (a,b) ∧ dist (x,b) ≤ dist (a,b)

⊢ (∀a b x.
     x ∈ segment [(a,b)] ⇒
     dist (x,a) ≤ dist (a,b) ∧ dist (x,b) ≤ dist (a,b)) ∧
  ∀a b x.
    x ∈ segment (a,b) ⇒ dist (x,a) < dist (a,b) ∧ dist (x,b) < dist (a,b)

⊢ ∀a b x.
    x ∈ segment (a,b) ⇒ dist (x,a) < dist (a,b) ∧ dist (x,b) < dist (a,b)

⊢ ∀a b.
    dist (a,midpoint (a,b)) = dist (a,b) / 2 ∧
    dist (b,midpoint (a,b)) = dist (a,b) / 2 ∧
    dist (midpoint (a,b),a) = dist (a,b) / 2 ∧
    dist (midpoint (a,b),b) = dist (a,b) / 2

⊢ ∀x y z.
    dist (x,z) = dist (x,y) + dist (y,z) ⇔
    abs (x − y) * (y − z) = abs (y − z) * (x − y)

⊢ ∅ = interval [(1,0)]

⊢ ∀s. FINITE s ⇒ interior s = ∅

⊢ (∀a b. a ∈ interval [(a,b)] ⇔ interval [(a,b)] ≠ ∅) ∧
  (∀a b. b ∈ interval [(a,b)] ⇔ interval [(a,b)] ≠ ∅) ∧
  (∀a b. a ∉ interval (a,b)) ∧ ∀a b. b ∉ interval (a,b)

⊢ ∀a b. a ∈ segment [(a,b)] ∧ b ∈ segment [(a,b)]

⊢ 0 ∈ interval [(0,1)] ∧ 1 ∈ interval [(0,1)] ∧ 0 ∉ interval (0,1) ∧
  1 ∉ interval (0,1)

⊢ ∀a b. a ∉ segment (a,b) ∧ b ∉ segment (a,b)

⊢ (∀a a' r r'. ball (a,r) = ball (a',r') ⇔ a = a' ∧ r = r' ∨ r ≤ 0 ∧ r' ≤ 0) ∧
  (∀a a' r r'. ball (a,r) = cball (a',r') ⇔ r ≤ 0 ∧ r' < 0) ∧
  (∀a a' r r'. cball (a,r) = ball (a',r') ⇔ r < 0 ∧ r' ≤ 0) ∧
  ∀a a' r r'.
    cball (a,r) = cball (a',r') ⇔ a = a' ∧ r = r' ∨ r < 0 ∧ r' < 0

⊢ (∀a b c d.
     interval [(a,b)] = interval [(c,d)] ⇔
     interval [(a,b)] = ∅ ∧ interval [(c,d)] = ∅ ∨ a = c ∧ b = d) ∧
  (∀a b c d.
     interval [(a,b)] = interval (c,d) ⇔
     interval [(a,b)] = ∅ ∧ interval (c,d) = ∅) ∧
  (∀a b c d.
     interval (a,b) = interval [(c,d)] ⇔
     interval (a,b) = ∅ ∧ interval [(c,d)] = ∅) ∧
  ∀a b c d.
    interval (a,b) = interval (c,d) ⇔
    interval (a,b) = ∅ ∧ interval (c,d) = ∅ ∨ a = c ∧ b = d

⊢ ∀a p.
    eventually p (at a) ⇔
    ∃d. 0 < d ∧ ∀x. 0 < dist (x,a) ∧ dist (x,a) < d ⇒ p x

⊢ ∀s a p.
    eventually p (at a within s) ⇔
    ∃d. 0 < d ∧ ∀x. x ∈ s ∧ 0 < dist (x,a) ∧ dist (x,a) < d ⇒ p x

⊢ ∀p s x.
    x ∈ interior s ⇒ (eventually p (at x within s) ⇔ eventually p (at x))

⊢ ∀s a p.
    eventually p (at a within s) ⇔
    ∃d. 0 < d ∧ ∀x. x ∈ s ∧ 0 < dist (x,a) ∧ dist (x,a) ≤ d ⇒ p x

⊢ ∀s t.
    FINITE t ∧ independent s ∧ s ⊆ span t ⇒
    ∃t'. t' HAS_SIZE CARD t ∧ s ⊆ t' ∧ t' ⊆ s ∪ t ∧ s ⊆ span t'

⊢ ∀s t. t ⊆ s ∧ s ≠ ∅ ∧ connected t ⇒ ∃c. c ∈ components s ∧ t ⊆ c

⊢ (∃s. P (𝕌(:α) DIFF s)) ⇔ ∃s. P s

⊢ ∀P a s. (∃x. x ∈ a INSERT s ∧ P x) ⇔ P a ∨ ∃x. x ∈ s ∧ P x

⊢ ∀f s t u.
    open_in (subtopology euclidean s) t ∧
    closed_in (subtopology euclidean s) t ∧ f continuous_on t ∧
    IMAGE f t ⊆ u ∧ (u = ∅ ⇒ s = ∅) ⇒
    ∃g. g continuous_on s ∧ IMAGE g s ⊆ u ∧ ∀x. x ∈ t ⇒ g x = f x

⊢ ∀a r. FINITE (ball (a,r)) ⇔ r ≤ 0

⊢ ∀a r. FINITE (cball (a,r)) ⇔ r ≤ 0

⊢ ∀s. FINITE s ⇒ bounded s

⊢ ∀s. FINITE s ⇒ closed s

⊢ ∀s t. FINITE s ∧ s ⊆ t ⇒ closed_in (subtopology euclidean t) s

⊢ ∀s. FINITE s ⇒ compact s

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ¬open s

⊢ (∀a b. FINITE (interval [(a,b)]) ⇔ b ≤ a) ∧
  ∀a b. FINITE (interval (a,b)) ⇔ b ≤ a

⊢ ∀s m n. FINITE (s ∩ {m .. n})

⊢ ∀a s. FINITE s ⇒ ∃d. 0 < d ∧ ∀x. x ∈ s ∧ x ≠ a ⇒ d ≤ dist (a,x)

⊢ ∀a r. FINITE (sphere (a,r))

⊢ ∀f s t.
    closed t ∧ f continuous_on closure s ∧ (∀x. x ∈ s ⇒ f x ∈ t) ⇒
    ∀x. x ∈ closure s ⇒ f x ∈ t

⊢ ∀f s t.
    closed t ∧ f continuous_on closure s ⇒
    ((∀x. x ∈ closure s ⇒ f x ∈ t) ⇔ ∀x. x ∈ s ⇒ f x ∈ t)

⊢ ∀a e. 0 < e ⇒ frontier (ball (a,e)) = sphere (a,e)

⊢ ∀a e. frontier (cball (a,e)) = sphere (a,e)

⊢ ∀s. closed (frontier s)

⊢ ∀a b. frontier (interval [(a,b)]) = interval [(a,b)] DIFF interval (a,b)

⊢ ∀s. frontier s = closure s ∩ closure (𝕌(:real) DIFF s)

⊢ ∀s. frontier (closure s) ⊆ frontier s

⊢ ∀s. frontier (𝕌(:real) DIFF s) = frontier s

⊢ ∀s. frontier s ∩ s = ∅ ⇔ open s

⊢ frontier ∅ = ∅

⊢ ∀s. open s ∨ closed s ⇒ frontier (frontier s) = frontier s

⊢ ∀s. frontier (frontier (frontier s)) = frontier (frontier s)

⊢ ∀s. frontier (frontier s) ⊆ frontier s

⊢ ∀a b. ¬(a = 0 ∧ b = 0) ⇒ frontier {x | a * x ≥ b} = {x | a * x = b}

⊢ ∀a b. ¬(a = 0 ∧ b = 0) ⇒ frontier {x | a * x > b} = {x | a * x = b}

⊢ ∀a b. ¬(a = 0 ∧ b = 0) ⇒ frontier {x | a * x ≤ b} = {x | a * x = b}

⊢ ∀a b. ¬(a = 0 ∧ b = 0) ⇒ frontier {x | a * x < b} = {x | a * x = b}

⊢ ∀s. frontier s = 𝕌(:real) DIFF interior s DIFF interior (𝕌(:real) DIFF s)

⊢ ∀s. frontier (interior s) ⊆ frontier s

⊢ ∀s t. frontier (s ∩ t) ⊆ frontier s ∪ frontier t

⊢ ∀s t. frontier (s ∩ t) ⊆ closure s ∩ frontier t ∪ frontier s ∩ closure t

⊢ ∀a b.
    frontier (interval (a,b)) =
    if interval (a,b) = ∅ then ∅ else interval [(a,b)] DIFF interval (a,b)

⊢ ∀a. frontier {a} = {a}

⊢ ∀a s.
    a ∈ frontier s ⇔
    ∀e. 0 < e ⇒ (∃x. x ∈ s ∧ dist (a,x) < e) ∧ ∃x. x ∉ s ∧ dist (a,x) < e

⊢ ∀s. closed s ⇒ frontier s ⊆ s

⊢ ∀s. compact s ⇒ frontier s ⊆ s

⊢ ∀s. frontier s ⊆ s ⇔ closed s

⊢ ∀s t.
    closure s ∩ closure t = ∅ ⇒ frontier (s ∪ t) = frontier s ∪ frontier t

⊢ ∀s t. frontier (s ∪ t) ⊆ frontier s ∪ frontier t

⊢ frontier 𝕌(:real) = ∅

⊢ ∀P f g.
    (∀x y. P x ∧ P y ∧ g x = g y ⇒ f x = f y) ⇔ ∃h. ∀x. P x ⇒ f x = h (g x)

⊢ ∀s. gdelta (𝕌(:real) DIFF s) ⇔ fsigma s

⊢ ∀m. m ≥ m

⊢ {i | 1 ≤ i ∧ i ≤ 1} HAS_SIZE 1

⊢ ∀s t.
    bounded s ∧ bounded t ∧ s ≠ ∅ ∧ t ≠ ∅ ⇒
    hausdist (s,t) =
    sup {abs (setdist ({x},s) − setdist ({x},t)) | x ∈ 𝕌(:real)}

⊢ (∀a b r s.
     hausdist (ball (a,r),ball (b,s)) =
     if r ≤ 0 ∨ s ≤ 0 then 0 else dist (a,b) + abs (r − s)) ∧
  (∀a b r s.
     hausdist (ball (a,r),cball (b,s)) =
     if r ≤ 0 ∨ s < 0 then 0 else dist (a,b) + abs (r − s)) ∧
  (∀a b r s.
     hausdist (cball (a,r),ball (b,s)) =
     if r < 0 ∨ s ≤ 0 then 0 else dist (a,b) + abs (r − s)) ∧
  ∀a b r s.
    hausdist (cball (a,r),cball (b,s)) =
    if r < 0 ∨ s < 0 then 0 else dist (a,b) + abs (r − s)

⊢ (∀s t. hausdist (closure s,t) = hausdist (s,t)) ∧
  ∀s t. hausdist (s,closure t) = hausdist (s,t)

⊢ ∀s t.
    bounded s ∧ compact t ∧ t ≠ ∅ ⇒
    ∀x. x ∈ s ⇒ ∃y. y ∈ t ∧ dist (x,y) ≤ hausdist (s,t)

⊢ ∀s t.
    compact s ∧ compact t ∧ s ≠ ∅ ∧ t ≠ ∅ ⇒
    hausdist (s,t) =
    inf
      {e |
       0 ≤ e ∧ s ⊆ {x + y | x ∈ t ∧ abs y ≤ e} ∧
       t ⊆ {x + y | x ∈ s ∧ abs y ≤ e}}

⊢ ∀s t.
    bounded s ∧ compact t ∧ t ≠ ∅ ⇒
    s ⊆ {y + z | y ∈ t ∧ z ∈ cball (0,hausdist (s,t))}

⊢ (∀t. hausdist (∅,t) = 0) ∧ ∀s. hausdist (s,∅) = 0

⊢ ∀s t s' t'.
    (∀b. (∀x. x ∈ s ⇒ setdist ({x},t) ≤ b) ∧
         (∀y. y ∈ t ⇒ setdist ({y},s) ≤ b) ⇔
         (∀x. x ∈ s' ⇒ setdist ({x},t') ≤ b) ∧
         ∀y. y ∈ t' ⇒ setdist ({y},s') ≤ b) ⇒
    hausdist (s,t) = hausdist (s',t')

⊢ ∀s t.
    bounded s ∧ bounded t ⇒
    (hausdist (s,t) = 0 ⇔ s = ∅ ∨ t = ∅ ∨ closure s = closure t)

⊢ ∀s t a.
    bounded s ∧ bounded t ∧ s ≠ ∅ ∧ t ≠ ∅ ⇒
    hausdist (a INSERT s,a INSERT t) ≤ hausdist (s,t)

⊢ ∀f s t.
    linear f ∧ (∀x. abs (f x) = abs x) ⇒
    hausdist (IMAGE f s,IMAGE f t) = hausdist (s,t)

⊢ ∀s t.
    bounded s ∧ bounded t ∧ s ≠ ∅ ∧ t ≠ ∅ ⇒
    hausdist (s,t) =
    sup ({setdist ({x},t) | x ∈ s} ∪ {setdist ({y},s) | y ∈ t})

⊢ ∀s t.
    bounded s ∧ bounded t ∧ s ≠ ∅ ∧ t ≠ ∅ ⇒
    hausdist (s,t) =
    max (sup {setdist ({x},t) | x ∈ s}) (sup {setdist ({y},s) | y ∈ t})

⊢ ∀s t. 0 ≤ hausdist (s,t)

⊢ ∀s. hausdist (s,s) = 0

⊢ ∀s t u.
    t ≠ ∅ ∧ bounded s ∧ bounded t ⇒
    setdist (s,u) ≤ hausdist (s,t) + setdist (t,u)

⊢ ∀x y. hausdist ({x},{y}) = dist (x,y)

⊢ ∀s t. hausdist (s,t) = hausdist (t,s)

⊢ ∀s t u.
    bounded s ∧ bounded t ∧ bounded u ∧ t ≠ ∅ ⇒
    hausdist (s,u) ≤ hausdist (s,t) + hausdist (t,u)

⊢ ∀a s t.
    hausdist (IMAGE (λx. a + x) s,IMAGE (λx. a + x) t) = hausdist (s,t)

⊢ ∀s t u.
    bounded s ∧ bounded t ∧ bounded u ∧ t ≠ ∅ ⇒
    hausdist (s,u) ≤ hausdist (s,t) + hausdist (t,u)

⊢ ∀s t u.
    bounded s ∧ bounded t ∧ bounded u ∧ t ≠ ∅ ∧ u ≠ ∅ ⇒
    hausdist (s ∪ t,s ∪ u) ≤ hausdist (t,u)

⊢ ∀s. (∀f. (∀t. t ∈ f ⇒ open t) ∧ s ⊆ BIGUNION f ⇒
           ∃f'. f' ⊆ f ∧ FINITE f' ∧ s ⊆ BIGUNION f') ⇒
      ∀t. INFINITE t ∧ t ⊆ s ⇒ ∃x. x ∈ s ∧ x limit_point_of t

⊢ ∀s. compact s ⇒
      ∀t. s ⊆ BIGUNION t ∧ (∀b. b ∈ t ⇒ open b) ⇒
          ∃e. 0 < e ∧ ∀x. x ∈ s ⇒ ∃b. b ∈ t ∧ ball (x,e) ⊆ b

⊢ ∀s a c. c ≠ 0 ⇒ s homeomorphic IMAGE (λx. a + c * x) s

⊢ ∀a b d e. 0 < d ∧ 0 < e ⇒ ball (a,d) homeomorphic ball (b,e)

⊢ (∀a b d e. 0 < d ∧ 0 < e ⇒ ball (a,d) homeomorphic ball (b,e)) ∧
  (∀a b d e. 0 < d ∧ 0 < e ⇒ cball (a,d) homeomorphic cball (b,e)) ∧
  ∀a b d e. 0 < d ∧ 0 < e ⇒ sphere (a,d) homeomorphic sphere (b,e)

⊢ ∀a b d e. 0 < d ∧ 0 < e ⇒ cball (a,d) homeomorphic cball (b,e)

⊢ ∀s f t.
    compact s ∧ f continuous_on s ∧ IMAGE f s = t ∧
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
    s homeomorphic t

⊢ ∀s t. s homeomorphic t ⇒ (compact s ⇔ compact t)

⊢ ∀s t. s homeomorphic t ⇒ (connected s ⇔ connected t)

⊢ (∀s. s homeomorphic ∅ ⇔ s = ∅) ∧ ∀s. ∅ homeomorphic s ⇔ s = ∅

⊢ ∀s t. FINITE s ∧ FINITE t ⇒ (s homeomorphic t ⇔ CARD s = CARD t)

⊢ ∀s t. s homeomorphic t ⇒ (FINITE s ⇔ FINITE t)

⊢ ∀s t.
    FINITE s ∨ FINITE t ⇒
    (s homeomorphic t ⇔ FINITE s ∧ FINITE t ∧ CARD s = CARD t)

⊢ ∀a b c d. a ≠ 0 ∧ c ≠ 0 ⇒ {x | a * x = b} homeomorphic {x | c * x = d}

⊢ ∀a b c. a ≠ 0 ⇒ {x | a * x = b} homeomorphic {x | x = c}

⊢ ∀s t. s homeomorphic t ⇒ s ≈ t

⊢ ∀f s t.
    linear f ∧ (∀x y. f x = f y ⇒ x = y) ⇒
    (IMAGE f s homeomorphic t ⇔ s homeomorphic t)

⊢ ∀f s t.
    linear f ∧ (∀x y. f x = f y ⇒ x = y) ⇒
    (s homeomorphic IMAGE f t ⇔ s homeomorphic t)

⊢ ∀f s. linear f ∧ (∀x y. f x = f y ⇒ x = y) ⇒ IMAGE f s homeomorphic s

⊢ ∀P Q.
    (∀s t. s homeomorphic t ⇒ (P s ⇔ Q t)) ⇒
    ∀s t. s homeomorphic t ⇒ (locally P s ⇔ locally Q t)

⊢ ∀s t. s homeomorphic t ⇒ (locally compact s ⇔ locally compact t)

⊢ ∀s t.
    s homeomorphic t ⇔
    ∃f g.
      (∀x. x ∈ s ⇒ f x ∈ t ∧ g (f x) = x) ∧
      (∀y. y ∈ t ⇒ g y ∈ s ∧ f (g y) = y) ∧ f continuous_on s ∧
      g continuous_on t

⊢ ∀s t a b.
    compact s ∧ compact t ∧ a ∈ s ∧ b ∈ t ∧
    s DELETE a homeomorphic t DELETE b ⇒
    s homeomorphic t

⊢ ∀a b c d. a < b ∧ c < d ⇒ interval (a,b) homeomorphic interval (c,d)

⊢ ∀a b. a < b ⇒ interval (a,b) homeomorphic 𝕌(:real)

⊢ ∀s. s homeomorphic s

⊢ ∀s c. c ≠ 0 ⇒ s homeomorphic IMAGE (λx. c * x) s

⊢ ∀c. 0 < c ⇒ ∀s t. IMAGE (λx. c * x) s homeomorphic t ⇔ s homeomorphic t

⊢ ∀c. 0 < c ⇒ ∀s t. s homeomorphic IMAGE (λx. c * x) t ⇔ s homeomorphic t

⊢ ∀a b. {a} homeomorphic {b}

⊢ ∀a b d e. 0 < d ∧ 0 < e ⇒ sphere (a,d) homeomorphic sphere (b,e)

⊢ ∀a b c. a ≠ 0 ⇒ {x | x = c} homeomorphic {x | a * x = b}

⊢ ∀s t. s homeomorphic t ⇔ t homeomorphic s

⊢ ∀s t u. s homeomorphic t ∧ t homeomorphic u ⇒ s homeomorphic u

⊢ ∀s a. s homeomorphic IMAGE (λx. a + x) s

⊢ ∀a s t. IMAGE (λx. a + x) s homeomorphic t ⇔ s homeomorphic t

⊢ ∀a s t. s homeomorphic IMAGE (λx. a + x) t ⇔ s homeomorphic t

⊢ ∀a s. IMAGE (λx. a + x) s homeomorphic s

⊢ ∀s t f g.
    homeomorphism (s,t) (f,g) ⇔
    f continuous_on s ∧ IMAGE f s ⊆ t ∧ g continuous_on t ∧ IMAGE g t ⊆ s ∧
    (∀x. x ∈ s ⇒ g (f x) = x) ∧ ∀y. y ∈ t ⇒ f (g y) = y

⊢ ∀s f t.
    compact s ∧ f continuous_on s ∧ IMAGE f s = t ∧
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
    ∃g. homeomorphism (s,t) (f,g)

⊢ ∀f g h k s t u.
    homeomorphism (s,t) (f,g) ∧ homeomorphism (t,u) (h,k) ⇒
    homeomorphism (s,u) (h ∘ f,g ∘ k)

⊢ ∀f g s t u.
    f continuous_on s ∧ IMAGE f s ⊆ t ∧ g continuous_on t ∧ IMAGE g t ⊆ u ∧
    (∀x y. x ∈ t ∧ y ∈ t ∧ g x = g y ⇒ x = y) ∧
    (∃h. homeomorphism (s,u) (g ∘ f,h)) ⇒
    (∃f'. homeomorphism (s,t) (f,f')) ∧ ∃g'. homeomorphism (t,u) (g,g')

⊢ ∀f g s t u.
    f continuous_on s ∧ IMAGE f s = t ∧ g continuous_on t ∧ IMAGE g t ⊆ u ∧
    (∃h. homeomorphism (s,u) (g ∘ f,h)) ⇒
    (∃f'. homeomorphism (s,t) (f,f')) ∧ ∃g'. homeomorphism (t,u) (g,g')

⊢ ∀s. homeomorphism (s,s) ((λx. x),(λx. x))

⊢ ∀f g s t u.
    homeomorphism (s,t) (f,g) ∧ closed_in (subtopology euclidean s) u ⇒
    closed_in (subtopology euclidean t) (IMAGE f u)

⊢ ∀f g s t u.
    homeomorphism (s,t) (f,g) ∧ open_in (subtopology euclidean s) u ⇒
    open_in (subtopology euclidean t) (IMAGE f u)

⊢ ∀f g s t.
    homeomorphism (s,t) (f,g) ⇒
    ∀u. u ⊆ t ⇒
        (open_in (subtopology euclidean s) {x | x ∈ s ∧ f x ∈ u} ⇔
         open_in (subtopology euclidean t) u)

⊢ ∀f s t.
    f continuous_on s ∧ IMAGE f s = t ∧
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ∧
    (∀u. closed_in (subtopology euclidean s) u ⇒
         closed_in (subtopology euclidean t) (IMAGE f u)) ⇒
    ∃g. homeomorphism (s,t) (f,g)

⊢ ∀f s t.
    f continuous_on s ∧ IMAGE f s = t ∧
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
    ((∃g. homeomorphism (s,t) (f,g)) ⇔
     ∀u. closed_in (subtopology euclidean s) u ⇒
         closed_in (subtopology euclidean t) (IMAGE f u))

⊢ ∀f s t.
    f continuous_on s ∧ IMAGE f s = t ∧
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ∧
    (∀u. open_in (subtopology euclidean s) u ⇒
         open_in (subtopology euclidean t) (IMAGE f u)) ⇒
    ∃g. homeomorphism (s,t) (f,g)

⊢ ∀f s t.
    f continuous_on s ∧ IMAGE f s = t ∧
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
    ((∃g. homeomorphism (s,t) (f,g)) ⇔
     ∀u. open_in (subtopology euclidean s) u ⇒
         open_in (subtopology euclidean t) (IMAGE f u))

⊢ ∀P Q f g.
    (∀s t. homeomorphism (s,t) (f,g) ⇒ (P s ⇔ Q t)) ⇒
    ∀s t. homeomorphism (s,t) (f,g) ⇒ (locally P s ⇔ locally Q t)

⊢ ∀f g s t s' t'.
    homeomorphism (s,t) (f,g) ∧ s' ⊆ s ∧ t' ⊆ t ∧ IMAGE f s' = t' ⇒
    homeomorphism (s',t') (f,g)

⊢ ∀f g s t. homeomorphism (s,t) (f,g) ⇔ homeomorphism (t,s) (g,f)

⊢ ∀a b m c.
    IMAGE (λx. m * x + c) (interval [(a,b)]) =
    if interval [(a,b)] = ∅ then ∅
    else if 0 ≤ m then interval [(m * a + c,m * b + c)]
    else interval [(m * b + c,m * a + c)]

⊢ ∀f s t.
    f continuous_on closure s ∧ closed t ∧ IMAGE f s ⊆ t ⇒
    IMAGE f (closure s) ⊆ t

⊢ ∀a b m.
    IMAGE (λx. @f. f = m 1 * x) (interval [(a,b)]) =
    if interval [(a,b)] = ∅ then ∅
    else
      interval
        [((@f. f = min (m 1 * a) (m 1 * b)),@f. f = max (m 1 * a) (m 1 * b))]

⊢ ∀p a b. IMAGE (λx. x) (interval [(a,b)]) = interval [(a,b)]

⊢ ∀s. independent s ⇒ FINITE s ∧ CARD s ≤ 1

⊢ ∀v b. b ⊆ v ∧ independent b ⇒ FINITE b ∧ CARD b ≤ dim v

⊢ independent ∅

⊢ ∀f s.
    independent s ∧ linear f ∧ (∀x y. f x = f y ⇒ x = y) ⇒
    independent (IMAGE f s)

⊢ ∀f s.
    independent s ∧ linear f ∧
    (∀x y. x ∈ span s ∧ y ∈ span s ∧ f x = f y ⇒ x = y) ⇒
    independent (IMAGE f s)

⊢ ∀a s.
    independent (a INSERT s) ⇔
    if a ∈ s then independent s else independent s ∧ a ∉ span s

⊢ ∀s t. independent t ∧ s ⊆ t ⇒ independent s

⊢ ∀s. independent s ⇒ 0 ∉ s

⊢ ∀x. independent {x} ⇔ x ≠ 0

⊢ ∀s t. FINITE t ∧ independent s ∧ s ⊆ span t ⇒ FINITE s ∧ CARD s ≤ CARD t

⊢ independent {i | 1 ≤ i ∧ i ≤ 1}

⊢ ∀u s.
    open_in (subtopology euclidean u) s ∧ (∃x. x ∈ s ∧ x limit_point_of u) ⇒
    INFINITE s

⊢ ∀s t. INFINITE s ∧ s ⊆ t ⇒ INFINITE t

⊢ suminf s (λi. 0) = 0

⊢ ∀x y s.
    summable s x ∧ summable s y ⇒
    suminf s (λi. x i + y i) = suminf s x + suminf s y

⊢ ∀s x c. summable s x ⇒ suminf s (λn. c * x n) = c * suminf s x

⊢ ∀f g k.
    summable k f ∧ summable k g ∧ (∀x. x ∈ k ⇒ f x = g x) ⇒
    suminf k f = suminf k g

⊢ ∀f h s. summable s f ∧ linear h ⇒ suminf s (λn. h (f n)) = h (suminf s f)

⊢ ∀s x. summable s x ⇒ suminf s (λn. -x n) = -suminf s x

⊢ ∀k a. suminf 𝕌(:num) (λn. if n ∈ k then a n else 0) = suminf k a

⊢ ∀x y s.
    summable s x ∧ summable s y ⇒
    suminf s (λi. x i − y i) = suminf s x − suminf s y

⊢ ∀f l s. (f sums l) s ⇒ suminf s f = l

⊢ ∀x s. bounded s ⇒ inf (x INSERT s) = if s = ∅ then x else min x (inf s)

⊢ ∀f s.
    closed s ∧ subspace s ∧ linear f ∧ (∀x. x ∈ s ∧ f x = 0 ⇒ x = 0) ⇒
    ∃e. 0 < e ∧ ∀x. x ∈ s ⇒ abs (f x) ≥ e * abs x

⊢ ∀f s t.
    f continuous_on s ∧ IMAGE f s = t ∧
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
    ((∀u. open_in (subtopology euclidean s) u ⇒
          open_in (subtopology euclidean t) (IMAGE f u)) ⇔
     ∀u. closed_in (subtopology euclidean s) u ⇒
         closed_in (subtopology euclidean t) (IMAGE f u))

⊢ ∀a r. interior (ball (a,r)) = ball (a,r)

⊢ ∀f. interior (BIGINTER f) ⊆ BIGINTER (IMAGE interior f)

⊢ ∀f s.
    linear f ∧ (∀x y. f x = f y ⇒ x = y) ∧ (∀y. ∃x. f x = y) ⇒
    interior (IMAGE f s) = IMAGE f (interior s)

⊢ ∀x e. interior (cball (x,e)) = ball (x,e)