Email Gateway (Feb 16 2026 at 13:59): Email Gateway (Feb 16 2026 at 13:59):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
We are excited to announce the initial alpha release of Isabelle/Copilot,
an AI-driven assistant for Isabelle/HOL. Copilot integrates foundation
models hosted on AWS Bedrock directly into the Isabelle/jEdit IDE,
providing both a dockable freeform chat interface and a dynamic,
right-click context menu for performing common theorem proving actions.
You can see Isabelle/Copilot in action via the GIFs embedded in the README,
here <https://github.com/awslabs/AutoCorrode/tree/main/isabelle-copilot>.
Currently around 30 separate actions, including explaining definitions and
theorems in natural language, refactoring apply-style proofs to Isar,
automatically generating introduction and elimination rules for
definitions, explaining simplifier traces, and an initial implementation of
an "auto prove" functionality, performing gradual refinement-style proof of
a goal, are implemented. More will follow.
Isabelle/Copilot is built atop the I/Q functionality that we open-sourced
last year, exposing Isabelle prover functionality to LLMs via an MCP
server. Copilot uses I/Q to check any proofs that it generates, refining
them iteratively in response to failures.
We welcome collaboration and contributions, including support for other
foundation model providers besides AWS.
Thanks,
Dominic and the AWS Bespoke Proofs team
Email Gateway (Feb 16 2026 at 14:09):From: Peter Lammich <lammich@in.tum.de>
Sounds good.
"
Prerequisites
<https://github.com/awslabs/AutoCorrode/tree/main/isabelle-copilot#prerequisites>
* Isabelle2025-2 <https://isabelle.in.tum.de/website-Isabelle2025-2/>
* AWS account withBedrock model access
<https://docs.aws.amazon.com/bedrock/latest/userguide/model-access.html>(Claude
recommended)
* AWS credentials configured (|~/.aws/credentials|or environment
variables)
"
So how do you get an "AWS account with Bedrock access" as a researcher,
and what does it cost? (There's not much information targeted at
researchers on the website behind the link)
--
Peter
On 16/02/2026 14:58, Dominic Mulligan (via cl-isabelle-users Mailing
List) wrote:
Dear all,
We are excited to announce the initial alpha release of
Isabelle/Copilot, an AI-driven assistant for Isabelle/HOL. Copilot
integrates foundation models hosted on AWS Bedrock directly into the
Isabelle/jEdit IDE, providing both a dockable freeform chat interface
and a dynamic, right-click context menu for performing common theorem
proving actions. You can see Isabelle/Copilot in action via the GIFs
embedded in the README, here
<https://github.com/awslabs/AutoCorrode/tree/main/isabelle-copilot>.Currently around 30 separate actions, including explaining definitions
and theorems in natural language, refactoring apply-style proofs to
Isar, automatically generating introduction and elimination rules for
definitions, explaining simplifier traces, and an initial
implementation of an "auto prove" functionality, performing gradual
refinement-style proof of a goal, are implemented. More will follow.Isabelle/Copilot is built atop the I/Q functionality that we
open-sourced last year, exposing Isabelle prover functionality to LLMs
via an MCP server. Copilot uses I/Q to check any proofs that it
generates, refining them iteratively in response to failures.We welcome collaboration and contributions, including support for
other foundation model providers besides AWS.Thanks,
Dominic and the AWS Bespoke Proofs team
Email Gateway (Feb 16 2026 at 14:26):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Quick rebrand after somebody pointed out we are probably too close to
Github Copilot: the tool is now called Isabelle Assistant!
On Mon, 16 Feb 2026 at 13:58, Dominic Mulligan <
dominic.p.mulligan@googlemail.com> wrote:
Dear all,
We are excited to announce the initial alpha release of Isabelle/Copilot,
an AI-driven assistant for Isabelle/HOL. Copilot integrates foundation
models hosted on AWS Bedrock directly into the Isabelle/jEdit IDE,
providing both a dockable freeform chat interface and a dynamic,
right-click context menu for performing common theorem proving actions.
You can see Isabelle/Copilot in action via the GIFs embedded in the README,
here <https://github.com/awslabs/AutoCorrode/tree/main/isabelle-copilot>.Currently around 30 separate actions, including explaining definitions and
theorems in natural language, refactoring apply-style proofs to Isar,
automatically generating introduction and elimination rules for
definitions, explaining simplifier traces, and an initial implementation of
an "auto prove" functionality, performing gradual refinement-style proof of
a goal, are implemented. More will follow.Isabelle/Copilot is built atop the I/Q functionality that we open-sourced
last year, exposing Isabelle prover functionality to LLMs via an MCP
server. Copilot uses I/Q to check any proofs that it generates, refining
them iteratively in response to failures.We welcome collaboration and contributions, including support for other
foundation model providers besides AWS.Thanks,
Dominic and the AWS Bespoke Proofs team
Email Gateway (Feb 16 2026 at 14:39):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi Peter,
To make use of Isabelle Assistant you will need to sign into the AWS
Console with a role that has Bedrock access (you can sign-up here
<https://docs.aws.amazon.com/bedrock/latest/userguide/getting-started.html> by
clicking the link in the top right-hand corner). Bedrock itself is
essentially pay-as-you-go with each LLM call being charged individually
(see e.g. here <https://aws.amazon.com/bedrock/pricing/>). Note according
to this, new AWS customers receive $200 of credit. Specifically for
researchers, we also have Amazon Research Awards which, if awarded, give
out AWS Credits as well. There is a dedicated Automated Reasoning ARA,
details of the last call here
<https://www.amazon.science/research-awards/call-for-proposals/automated-reasoning-call-for-proposals-fall-2025>
.
Thanks,
Dominic
On Mon, 16 Feb 2026 at 14:08, Peter Lammich <lammich@in.tum.de> wrote:
Sounds good.
"
Prerequisites
<https://github.com/awslabs/AutoCorrode/tree/main/isabelle-copilot#prerequisites>- Isabelle2025-2 <https://isabelle.in.tum.de/website-Isabelle2025-2/>
- AWS account with Bedrock model access
<https://docs.aws.amazon.com/bedrock/latest/userguide/model-access.html>
(Claude recommended)
- AWS credentials configured (~/.aws/credentials or environment
variables)"
So how do you get an "AWS account with Bedrock access" as a researcher,
and what does it cost? (There's not much information targeted at
researchers on the website behind the link)--
Peter
On 16/02/2026 14:58, Dominic Mulligan (via cl-isabelle-users Mailing List)
wrote:Dear all,
We are excited to announce the initial alpha release of Isabelle/Copilot,
an AI-driven assistant for Isabelle/HOL. Copilot integrates foundation
models hosted on AWS Bedrock directly into the Isabelle/jEdit IDE,
providing both a dockable freeform chat interface and a dynamic,
right-click context menu for performing common theorem proving actions.
You can see Isabelle/Copilot in action via the GIFs embedded in the README,
here <https://github.com/awslabs/AutoCorrode/tree/main/isabelle-copilot>.Currently around 30 separate actions, including explaining definitions and
theorems in natural language, refactoring apply-style proofs to Isar,
automatically generating introduction and elimination rules for
definitions, explaining simplifier traces, and an initial implementation of
an "auto prove" functionality, performing gradual refinement-style proof of
a goal, are implemented. More will follow.Isabelle/Copilot is built atop the I/Q functionality that we open-sourced
last year, exposing Isabelle prover functionality to LLMs via an MCP
server. Copilot uses I/Q to check any proofs that it generates, refining
them iteratively in response to failures.We welcome collaboration and contributions, including support for other
foundation model providers besides AWS.Thanks,
Dominic and the AWS Bespoke Proofs team
Email Gateway (Feb 20 2026 at 09:30):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
As a follow up to this—as there's been rapid development of this plugin
over the last week—I'm attaching the text of a theory file containing a
proof of the Urysohn metrization theorem. The proof follows the argument
set forth by Monkres in the book, Topology. It was developed by Larry
yesterday using Isabelle Assistant, which proved the result in about 2.5
hours with Larry feeding text taken from the book. Larry was able to do
other things whilst it autoformalized the material in the background. Once
it approached the end of the proof the agent realized it knew enough to go
ahead and finish the proof itself without further prompting. This was
using the new Claude Opus 4.6 model.
Note we chose this proof as a stress-testing example as we are aware of
similar tests being done by Josef Urban and John Harrison within the
context of different theorem proving systems.
theory Urysohn_Met3 imports "HOL-Analysis.Analysis"
"Isabelle_Assistant.Assistant_Support" begin
lemma metrizable_space_countable_product_of_reals:
shows ‹metrizable_space (product_topology (λ_::nat. euclideanreal) UNIV)›
by (simp add: euclidean_product_topology metrizable_space_euclidean)
theorem Urysohn_metrization:
fixes X :: ‹'a topology›
assumes ‹regular_space X› and ‹second_countable X› and ‹t1_space X› shows
‹metrizable_space X›
proof -
― ‹Obtain a countable basis for X›
obtain ℬ where ℬ_count: ‹countable ℬ›
and ℬ_open: ‹∀V ∈ ℬ. openin X V›
and ℬ_base: ‹∀U x. openin X U ∧ x ∈ U ⟶ (∃V ∈ ℬ. x ∈ V ∧ V ⊆ U)›
using assms(2) second_countable_def by metis
― ‹X is normal (regular + Lindelöf ⟹ normal)›
have normal: ‹normal_space X›
using assms regular_Lindelof_imp_normal_space
second_countable_imp_Lindelof_space by blast
― ‹For each pair (Bn, Bm) from the basis with closure of Bn ⊆ Bm,
apply Urysohn's lemma to obtain g Bn Bm : X → [0,1] continuous with
g Bn Bm (X closure_of Bn) ⊆ {1} and g Bn Bm (topspace X - Bm) ⊆
{0}›
define pairs where ‹pairs ≡ {(Bn, Bm). Bn ∈ ℬ ∧ Bm ∈ ℬ ∧ X closure_of Bn
⊆ Bm}›
have pairs_count: ‹countable pairs›
unfolding pairs_def using ℬ_count by (auto intro: countable_subset[OF _
countable_SIGMA[OF ℬ_count]])
have ‹∀(Bn, Bm) ∈ pairs.
∃g::'a⇒real. continuous_map X (top_of_set {0..1}) g ∧
g (topspace X - Bm) ⊆ {0} ∧
g (X closure_of Bn) ⊆ {1}›
proof (clarsimp simp: pairs_def)
fix Bn Bm
assume Bn_in: ‹Bn ∈ ℬ› and Bm_in: ‹Bm ∈ ℬ› and sub: ‹X closure_of Bn ⊆
Bm›
have cl_closed: ‹closedin X (X closure_of Bn)›
by (rule closedin_closure_of)
have comp_closed: ‹closedin X (topspace X - Bm)›
using ℬ_open Bm_in by (simp add: closedin_diff)
have disj: ‹disjnt (topspace X - Bm) (X closure_of Bn)›
using sub closure_of_subset_topspace by (fastforce simp: disjnt_iff)
show ‹∃g::'a⇒real. continuous_map X (top_of_set {0..1}) g ∧
g (topspace X - Bm) ⊆ {0} ∧
g (X closure_of Bn) ⊆ {1}›
using normal[unfolded normal_space_iff_Urysohn] comp_closed cl_closed
disj by blast
qed
then have ‹∀p ∈ pairs.
∃g::'a⇒real. continuous_map X (top_of_set {0..1}) g ∧
g (topspace X - snd p) ⊆ {0} ∧
g (X closure_of fst p) ⊆ {1}›
by (auto simp: case_prod_unfold)
then obtain gp where gp: ‹⋀p. p ∈ pairs ⟹
continuous_map X (top_of_set {0..1::real}) (gp p) ∧
gp p (topspace X - snd p) ⊆ {0} ∧
gp p (X closure_of fst p) ⊆ {1}›
by (meson bchoice)
define g where ‹g ≡ λBn Bm. gp (Bn, Bm)›
have g_cont: ‹⋀Bn Bm. (Bn, Bm) ∈ pairs ⟹
continuous_map X (top_of_set {0..1::real}) (g Bn Bm)›
and g_zero: ‹⋀Bn Bm. (Bn, Bm) ∈ pairs ⟹
g Bn Bm (topspace X - Bm) ⊆ {0}›
and g_one: ‹⋀Bn Bm. (Bn, Bm) ∈ pairs ⟹
g Bn Bm (X closure_of Bn) ⊆ {1}›
using gp unfolding g_def by (fastforce simp: image_subset_iff)+
― ‹The separation property of the family {g Bn Bm}: for any x0 in X and
any open neighbourhood U of x0, there exist Bn, Bm in the basis with
(Bn, Bm) ∈ pairs, g Bn Bm x0 = 1 > 0, and g Bn Bm vanishes outside U.›
have separation: ‹∃Bn Bm. (Bn, Bm) ∈ pairs ∧ g Bn Bm x0 = 1 ∧
(∀x ∈ topspace X - U. g Bn Bm x = 0)›
if ‹openin X U› and ‹x0 ∈ U› for x0 U
proof -
― ‹Step 1: choose basis element Bm with x0 ∈ Bm ⊆ U›
obtain Bm where Bm_in: ‹Bm ∈ ℬ› and x0_Bm: ‹x0 ∈ Bm› and Bm_sub: ‹Bm ⊆
U›
using ℬ_base that ‹openin X U› ‹x0 ∈ U› by blast
― ‹Step 2: by regularity, find open U' and closed V with x0 ∈ U' ⊆ V ⊆
Bm›
have ‹x0 ∈ topspace X›
using that openin_subset by blast
then obtain U' V where U'_open: ‹openin X U'› and V_closed: ‹closedin X
V›
and x0_U': ‹x0 ∈ U'› and U'_V: ‹U' ⊆ V› and V_Bm: ‹V ⊆ Bm›
using assms(1)[unfolded neighbourhood_base_of_closedin[symmetric]
neighbourhood_base_of_def neighbourhood_base_at_def]
ℬ_open Bm_in x0_Bm by meson
― ‹Step 3: choose basis element Bn with x0 ∈ Bn ⊆ U'›
obtain Bn where Bn_in: ‹Bn ∈ ℬ› and x0_Bn: ‹x0 ∈ Bn› and Bn_sub: ‹Bn ⊆
U'›
using ℬ_base U'_open x0_U' by blast
― ‹Bn ⊆ U' ⊆ V (closed), so closure_of Bn ⊆ V ⊆ Bm›
have cl_Bn_Bm: ‹X closure_of Bn ⊆ Bm›
using Bn_sub U'_V V_Bm V_closed closure_of_minimal by (meson
order_trans)
― ‹Hence (Bn, Bm) ∈ pairs›
have pair_in: ‹(Bn, Bm) ∈ pairs›
unfolding pairs_def using Bn_in Bm_in cl_Bn_Bm by blast
― ‹g Bn Bm x0 = 1 since x0 ∈ Bn ⊆ closure_of Bn›
have ‹x0 ∈ X closure_of Bn›
using x0_Bn closure_of_subset openin_subset ℬ_open Bn_in by (meson
in_mono)
then have ‹g Bn Bm x0 = 1›
using g_one[OF pair_in] by (auto simp: image_subset_iff)
― ‹g Bn Bm vanishes outside U since X - U ⊆ X - Bm›
moreover have ‹∀x ∈ topspace X - U. g Bn Bm x = 0›
using g_zero[OF pair_in] Bm_sub by (fastforce simp: image_subset_iff)
ultimately show ?thesis
using pair_in by blast
qed
― ‹Reindex the countable family {gp p | p ∈ pairs} with natural numbers.
Since pairs is countable, we can enumerate it using from_nat_into.›
define f where ‹f ≡ λn. gp (from_nat_into pairs n)›
have f_cont: ‹continuous_map X (top_of_set {0..1::real}) (f n)›
if ‹pairs ≠ {}› for n
using gp from_nat_into[OF that] unfolding f_def by blast
have f_surj: ‹∀p ∈ pairs. ∃n. f n = gp p›
using from_nat_into_surj[OF pairs_count] unfolding f_def by metis
― ‹The key separation property of the reindexed family:
for any x0 ∈ X and open U ∋ x0, there exists n with f n x0 > 0
and f n vanishing outside U.›
have f_sep: ‹∃n. f n x0 > 0 ∧ (∀x ∈ topspace X - U. f n x = 0)›
if ‹openin X U› and ‹x0 ∈ U› for x0 U
proof -
obtain Bn Bm where pair_in: ‹(Bn, Bm) ∈ pairs›
and val1: ‹g Bn Bm x0 = 1› and van: ‹∀x ∈ topspace X - U. g Bn Bm x =
0›
using separation that ‹openin X U› ‹x0 ∈ U› by blast
obtain n where fn: ‹f n = gp (Bn, Bm)›
using f_surj pair_in by blast
have ‹f n = g Bn Bm›
unfolding g_def using fn by simp
then have ‹f n x0 > 0 ∧ (∀x ∈ topspace X - U. f n x = 0)›
using val1 van by simp
then show ?thesis
by blast
qed ― ‹Define F : X → ℝ^ω by F(x) = (f 0 x, f 1 x, f 2 x, ...)›
define F where ‹F ≡ λx. λn. f n x›
― ‹If the topspace is nonempty, pairs is nonempty.›
have pairs_nonempty: ‹pairs ≠ {}› if ‹topspace X ≠ {}›
using separation that by blast
― ‹F is continuous: ℝ^ω has the product topology, so it suffices
to show each component f n is continuous as a map X → ℝ.›
have F_cont: ‹continuous_map X (product_topology (λ_::nat. euclideanreal)
UNIV) F›
if nonempty: ‹topspace X ≠ {}›
proof -
have ‹continuous_map X euclideanreal (f n)› for n
using f_cont[OF pairs_nonempty[OF nonempty]]
by (rule continuous_map_into_fulltopology)
then show ?thesis
unfolding F_def
by (subst continuous_map_componentwise_UNIV) auto
qed
― ‹F is injective: given x ≠ y in X, since X is T1 there is an
open set U containing y but not x. By f_sep there exists n
with f n y > 0 and f n x = 0, so F x ≠ F y.›
have F_inj: ‹inj_on F (topspace X)›
proof (rule inj_onI)
fix x y
assume xX: ‹x ∈ topspace X› and yX: ‹y ∈ topspace X› and Feq: ‹F x = F
y›
show ‹x = y›
proof (rule ccontr)
assume ‹x ≠ y›
― ‹By T1, there exists an open set U containing y but not x›
then obtain U where U_open: ‹openin X U› and yU: ‹y ∈ U› and xU: ‹x ∉
U›
using ‹t1_space X›[unfolded t1_space_def, rule_format, OF yX xX] by
auto
― ‹By f_sep, there exists n with f n y > 0 and f n x = 0›
then obtain n where ‹f n y > 0› and ‹f n x = 0›
using f_sep[OF U_open yU] xU xX by auto
― ‹But F x = F y means f n x = f n y for all n, contradiction›
then have ‹F x n ≠ F y n›
unfolding F_def by simp
then show False using Feq by (simp add: fun_eq_iff)
qed
qed
show ‹metrizable_space X›
proof (cases ‹topspace X = {}›)
case True
then show ?thesis
using null_topspace_iff_trivial empty_metrizable_space by metis
next
case nonempty: False
then have ne: ‹topspace X ≠ {}› by simp
let ?Y = ‹product_topology (λ_::nat. euclideanreal) UNIV›
have ts_Y: ‹topspace ?Y = UNIV›
by simp have F_open: ‹open_map X (subtopology ?Y (F topspace X))
F›
proof (unfold open_map_def, intro allI impI)
fix U assume U_open: ‹openin X U›
show ‹openin (subtopology ?Y (F topspace X)) (F U)›
proof (subst openin_subopen, intro ballI)
fix y assume ‹y ∈ F U›
then obtain x0 where x0U: ‹x0 ∈ U› and y_eq: ‹y = F x0› by auto
obtain n where fn_pos: ‹f n x0 > 0› and fn_van: ‹∀x ∈ topspace X -
U. f n x = 0›
using f_sep[OF U_open x0U] by auto
― ‹The set W = {z ∈ topspace Y. z n > 0} is open in Y›
let ?W = ‹{z ∈ topspace ?Y. z n ∈ {0<..}}›
have W_open: ‹openin ?Y ?W›
by (rule openin_continuo
[message truncated]
Email Gateway (Feb 20 2026 at 10:22):From: Tobias Nipkow <nipkow@in.tum.de>
Dominic,
I have followed the recent work by Urban and Harrison a little and am delighted
to see that you are providing similar functionality in Isabelle, with comparable
results. Thank you!
Tobias
On 20/02/2026 10:29, Dominic Mulligan (via cl-isabelle-users Mailing List) wrote:
As a follow up to this—as there's been rapid development of this plugin over the
last week—I'm attaching the text of a theory file containing a proof of the
Urysohn metrization theorem. The proof follows the argument set forth by
Monkres in the book, Topology. It was developed by Larry yesterday using
Isabelle Assistant, which proved the result in about 2.5 hours with Larry
feeding text taken from the book. Larry was able to do other things whilst it
autoformalized the material in the background. Once it approached the end of
the proof the agent realized it knew enough to go ahead and finish the proof
itself without further prompting. This was using the new Claude Opus 4.6 model.Note we chose this proof as a stress-testing example as we are aware of similar
tests being done by Josef Urban and John Harrison within the context of
different theorem proving systems.theory Urysohn_Met3 imports "HOL-Analysis.Analysis"
"Isabelle_Assistant.Assistant_Support" beginlemma metrizable_space_countable_product_of_reals:
shows ‹metrizable_space (product_topology (λ_::nat. euclideanreal) UNIV)›
by (simp add: euclidean_product_topology metrizable_space_euclidean)theorem Urysohn_metrization:
fixes X :: ‹'a topology›
assumes ‹regular_space X› and ‹second_countable X› and ‹t1_space X› shows
‹metrizable_space X›
proof -
― ‹Obtain a countable basis for X›
obtain ℬ where ℬ_count: ‹countable ℬ›
and ℬ_open: ‹∀V ∈ ℬ. openin X V›
and ℬ_base: ‹∀U x. openin X U ∧ x ∈ U ⟶ (∃V ∈ ℬ. x ∈ V ∧ V ⊆ U)›
using assms(2) second_countable_def by metis
― ‹X is normal (regular + Lindelöf ⟹ normal)›
have normal: ‹normal_space X›
using assms regular_Lindelof_imp_normal_space
second_countable_imp_Lindelof_space by blast
― ‹For each pair (Bn, Bm) from the basis with closure of Bn ⊆ Bm,
apply Urysohn's lemma to obtain g Bn Bm : X → [0,1] continuous with
g Bn Bm(X closure_of Bn) ⊆ {1} and g Bn Bm(topspace X - Bm) ⊆ {0}›
define pairs where ‹pairs ≡ {(Bn, Bm). Bn ∈ ℬ ∧ Bm ∈ ℬ ∧ X closure_of Bn ⊆ Bm}›
have pairs_count: ‹countable pairs›
unfolding pairs_def using ℬ_count by (auto intro: countable_subset[OF _
countable_SIGMA[OF ℬ_count]])
have ‹∀(Bn, Bm) ∈ pairs.
∃g::'a⇒real. continuous_map X (top_of_set {0..1}) g ∧
g(topspace X - Bm) ⊆ {0} ∧ g(X closure_of Bn) ⊆ {1}›
proof (clarsimp simp: pairs_def)
fix Bn Bm
assume Bn_in: ‹Bn ∈ ℬ› and Bm_in: ‹Bm ∈ ℬ› and sub: ‹X closure_of Bn ⊆ Bm›
have cl_closed: ‹closedin X (X closure_of Bn)›
by (rule closedin_closure_of)
have comp_closed: ‹closedin X (topspace X - Bm)›
using ℬ_open Bm_in by (simp add: closedin_diff)
have disj: ‹disjnt (topspace X - Bm) (X closure_of Bn)›
using sub closure_of_subset_topspace by (fastforce simp: disjnt_iff)
show ‹∃g::'a⇒real. continuous_map X (top_of_set {0..1}) g ∧
g(topspace X - Bm) ⊆ {0} ∧ g(X closure_of Bn) ⊆ {1}›
using normal[unfolded normal_space_iff_Urysohn] comp_closed cl_closed
disj by blast
qed
then have ‹∀p ∈ pairs.
∃g::'a⇒real. continuous_map X (top_of_set {0..1}) g ∧
g(topspace X - snd p) ⊆ {0} ∧ g(X closure_of fst p) ⊆ {1}›
by (auto simp: case_prod_unfold)
then obtain gp where gp: ‹⋀p. p ∈ pairs ⟹
continuous_map X (top_of_set {0..1::real}) (gp p) ∧
gp p(topspace X - snd p) ⊆ {0} ∧ gp p(X closure_of fst p) ⊆ {1}›
by (meson bchoice)
define g where ‹g ≡ λBn Bm. gp (Bn, Bm)›
have g_cont: ‹⋀Bn Bm. (Bn, Bm) ∈ pairs ⟹
continuous_map X (top_of_set {0..1::real}) (g Bn Bm)›
and g_zero: ‹⋀Bn Bm. (Bn, Bm) ∈ pairs ⟹
g Bn Bm(topspace X - Bm) ⊆ {0}› and g_one: ‹⋀Bn Bm. (Bn, Bm) ∈ pairs ⟹ g Bn Bm(X closure_of Bn) ⊆ {1}›
using gp unfolding g_def by (fastforce simp: image_subset_iff)+
― ‹The separation property of the family {g Bn Bm}: for any x0 in X and
any open neighbourhood U of x0, there exist Bn, Bm in the basis with
(Bn, Bm) ∈ pairs, g Bn Bm x0 = 1 > 0, and g Bn Bm vanishes outside U.›
have separation: ‹∃Bn Bm. (Bn, Bm) ∈ pairs ∧ g Bn Bm x0 = 1 ∧
(∀x ∈ topspace X - U. g Bn Bm x = 0)›
if ‹openin X U› and ‹x0 ∈ U› for x0 U
proof -
― ‹Step 1: choose basis element Bm with x0 ∈ Bm ⊆ U›
obtain Bm where Bm_in: ‹Bm ∈ ℬ› and x0_Bm: ‹x0 ∈ Bm› and Bm_sub: ‹Bm ⊆ U›
using ℬ_base that ‹openin X U› ‹x0 ∈ U› by blast
― ‹Step 2: by regularity, find open U' and closed V with x0 ∈ U' ⊆ V ⊆ Bm›
have ‹x0 ∈ topspace X›
using that openin_subset by blast
then obtain U' V where U'_open: ‹openin X U'› and V_closed: ‹closedin X V›
and x0_U': ‹x0 ∈ U'› and U'_V: ‹U' ⊆ V› and V_Bm: ‹V ⊆ Bm›
using assms(1)[unfolded neighbourhood_base_of_closedin[symmetric]
neighbourhood_base_of_def neighbourhood_base_at_def]
ℬ_open Bm_in x0_Bm by meson
― ‹Step 3: choose basis element Bn with x0 ∈ Bn ⊆ U'›
obtain Bn where Bn_in: ‹Bn ∈ ℬ› and x0_Bn: ‹x0 ∈ Bn› and Bn_sub: ‹Bn ⊆ U'›
using ℬ_base U'_open x0_U' by blast
― ‹Bn ⊆ U' ⊆ V (closed), so closure_of Bn ⊆ V ⊆ Bm›
have cl_Bn_Bm: ‹X closure_of Bn ⊆ Bm›
using Bn_sub U'_V V_Bm V_closed closure_of_minimal by (meson order_trans)
― ‹Hence (Bn, Bm) ∈ pairs›
have pair_in: ‹(Bn, Bm) ∈ pairs›
unfolding pairs_def using Bn_in Bm_in cl_Bn_Bm by blast
― ‹g Bn Bm x0 = 1 since x0 ∈ Bn ⊆ closure_of Bn›
have ‹x0 ∈ X closure_of Bn›
using x0_Bn closure_of_subset openin_subset ℬ_open Bn_in by (meson in_mono)
then have ‹g Bn Bm x0 = 1›
using g_one[OF pair_in] by (auto simp: image_subset_iff)
― ‹g Bn Bm vanishes outside U since X - U ⊆ X - Bm›
moreover have ‹∀x ∈ topspace X - U. g Bn Bm x = 0›
using g_zero[OF pair_in] Bm_sub by (fastforce simp: image_subset_iff)
ultimately show ?thesis
using pair_in by blast
qed
― ‹Reindex the countable family {gp p | p ∈ pairs} with natural numbers.
Since pairs is countable, we can enumerate it using from_nat_into.›
define f where ‹f ≡ λn. gp (from_nat_into pairs n)›
have f_cont: ‹continuous_map X (top_of_set {0..1::real}) (f n)›
if ‹pairs ≠ {}› for n
using gp from_nat_into[OF that] unfolding f_def by blast
have f_surj: ‹∀p ∈ pairs. ∃n. f n = gp p›
using from_nat_into_surj[OF pairs_count] unfolding f_def by metis
― ‹The key separation property of the reindexed family:
for any x0 ∈ X and open U ∋ x0, there exists n with f n x0 > 0
and f n vanishing outside U.›
have f_sep: ‹∃n. f n x0 > 0 ∧ (∀x ∈ topspace X - U. f n x = 0)›
if ‹openin X U› and ‹x0 ∈ U› for x0 U
proof -
obtain Bn Bm where pair_in: ‹(Bn, Bm) ∈ pairs›
and val1: ‹g Bn Bm x0 = 1› and van: ‹∀x ∈ topspace X - U. g Bn Bm x = 0›
using separation that ‹openin X U› ‹x0 ∈ U› by blast
obtain n where fn: ‹f n = gp (Bn, Bm)›
using f_surj pair_in by blast
have ‹f n = g Bn Bm›
unfolding g_def using fn by simp
then have ‹f n x0 > 0 ∧ (∀x ∈ topspace X - U. f n x = 0)›
using val1 van by simp
then show ?thesis
by blast
qed ― ‹Define F : X → ℝ^ω by F(x) = (f 0 x, f 1 x, f 2 x, ...)›
define F where ‹F ≡ λx. λn. f n x›
― ‹If the topspace is nonempty, pairs is nonempty.›
have pairs_nonempty: ‹pairs ≠ {}› if ‹topspace X ≠ {}›
using separation that by blast
― ‹F is continuous: ℝ^ω has the product topology, so it suffices
to show each component f n is continuous as a map X → ℝ.›
have F_cont: ‹continuous_map X (product_topology (λ_::nat. euclideanreal)
UNIV) F›
if nonempty: ‹topspace X ≠ {}›
proof -
have ‹continuous_map X euclideanreal (f n)› for n
using f_cont[OF pairs_nonempty[OF nonempty]]
by (rule continuous_map_into_fulltopology)
then show ?thesis
unfolding F_def
by (subst continuous_map_componentwise_UNIV) auto
qed
― ‹F is injective: given x ≠ y in X, since X is T1 there is an
open set U containing y but not x. By f_sep there exists n
with f n y > 0 and f n x = 0, so F x ≠ F y.›
have F_inj: ‹inj_on F (topspace X)›
proof (rule inj_onI)
fix x y
assume xX: ‹x ∈ topspace X› and yX: ‹y ∈ topspace X› and Feq: ‹F x = F y›
show ‹x = y›
proof (rule ccontr)
assume ‹x ≠ y›
― ‹By T1, there exists an open set U containing y but not x›
then obtain U where U_open: ‹openin X U› and yU: ‹y ∈ U› and xU: ‹x ∉ U›
using ‹t1_space X›[unfolded t1_space_def, rule_format, OF yX xX] by auto
― ‹By f_sep, there exists n with f n y > 0 and f n x = 0›
then obtain n where ‹f n y > 0› and ‹f n x = 0›
using f_sep[OF U_open yU] xU xX by auto
― ‹But F x = F y means f n x = f n y for all n, contradiction›
then have ‹F x n ≠ F y n›
unfolding F_def by simp
then show False using Feq by (simp add: fun_eq_iff)[message truncated]
smime.p7s
Last updated: Feb 22 2026 at 05:16 UTC