[STATEMENT]
lemma nhds_prod: "nhds (a, b) = nhds a \<times>\<^sub>F nhds b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nhds (a, b) = nhds a \<times>\<^sub>F nhds b
[PROOF STEP]
unfolding nhds_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf (principal ` {S. open S \<and> (a, b) \<in> S}) = Inf (principal ` {S. open S \<and> a \<in> S}) \<times>\<^sub>F Inf (principal ` {S. open S \<and> b \<in> S})
[PROOF STEP]
proof (subst prod_filter_INF, auto intro!: antisym INF_greatest simp: principal_prod_principal)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>open x; a \<in> x; open xa; b \<in> xa\<rbrakk> \<Longrightarrow> Inf (principal ` {S. open S \<and> (a, b) \<in> S}) \<le> principal (x \<times> xa)
 2. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
fix S T
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>open x; a \<in> x; open xa; b \<in> xa\<rbrakk> \<Longrightarrow> Inf (principal ` {S. open S \<and> (a, b) \<in> S}) \<le> principal (x \<times> xa)
 2. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
assume "open S" "a \<in> S" "open T" "b \<in> T"
[PROOF STATE]
proof (state)
this:
open S
a \<in> S
open T
b \<in> T

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>open x; a \<in> x; open xa; b \<in> xa\<rbrakk> \<Longrightarrow> Inf (principal ` {S. open S \<and> (a, b) \<in> S}) \<le> principal (x \<times> xa)
 2. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open S
a \<in> S
open T
b \<in> T
[PROOF STEP]
show "(INF x \<in> {S. open S \<and> (a, b) \<in> S}. principal x) \<le> principal (S \<times> T)"
[PROOF STATE]
proof (prove)
using this:
open S
a \<in> S
open T
b \<in> T

goal (1 subgoal):
 1. Inf (principal ` {S. open S \<and> (a, b) \<in> S}) \<le> principal (S \<times> T)
[PROOF STEP]
by (intro INF_lower) (auto intro!: open_Times)
[PROOF STATE]
proof (state)
this:
Inf (principal ` {S. open S \<and> (a, b) \<in> S}) \<le> principal (S \<times> T)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
fix S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
assume "open S'" "(a, b) \<in> S'"
[PROOF STATE]
proof (state)
this:
open S'
(a, b) \<in> S'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open S'
(a, b) \<in> S'
[PROOF STEP]
obtain S T where "open S" "a \<in> S" "open T" "b \<in> T" "S \<times> T \<subseteq> S'"
[PROOF STATE]
proof (prove)
using this:
open S'
(a, b) \<in> S'

goal (1 subgoal):
 1. (\<And>S T. \<lbrakk>open S; a \<in> S; open T; b \<in> T; S \<times> T \<subseteq> S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: open_prod_elim)
[PROOF STATE]
proof (state)
this:
open S
a \<in> S
open T
b \<in> T
S \<times> T \<subseteq> S'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open S
a \<in> S
open T
b \<in> T
S \<times> T \<subseteq> S'
[PROOF STEP]
show "(INF x \<in> {S. open S \<and> a \<in> S}. INF y \<in> {S. open S \<and> b \<in> S}.
      principal (x \<times> y)) \<le> principal S'"
[PROOF STATE]
proof (prove)
using this:
open S
a \<in> S
open T
b \<in> T
S \<times> T \<subseteq> S'

goal (1 subgoal):
 1. (INF x\<in>{S. open S \<and> a \<in> S}. INF y\<in>{S. open S \<and> b \<in> S}. principal (x \<times> y)) \<le> principal S'
[PROOF STEP]
by (auto intro!: INF_lower2)
[PROOF STATE]
proof (state)
this:
(INF x\<in>{S. open S \<and> a \<in> S}. INF y\<in>{S. open S \<and> b \<in> S}. principal (x \<times> y)) \<le> principal S'

goal:
No subgoals!
[PROOF STEP]
qed