:: On the {B}orel Families of Subsets of Topological Spaces
::  by Adam Grabowski
::
:: Received August 30, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies STRUCT_0, SETFAM_1, ZFMISC_1, CARD_3, TARSKI, NUMBERS, FUNCT_1,
      RELAT_1, CARD_1, ORDINAL1, SUBSET_1, XBOOLE_0, PRE_TOPC, TOPGEN_1,
      FINSET_1, WAYBEL23, RCOMP_1, RLVECT_3, TOPS_1, CONNSP_1, PCOMPS_1,
      NATTRA_1, PROB_1, MEASURE1, MCART_1, TOPMETR, CONNSP_2, WAYBEL30,
      OPENLATT, EQREL_1, NAT_1, TOPGEN_4;
 notations TARSKI, XBOOLE_0, XTUPLE_0, XFAMILY, SUBSET_1, RELAT_1, FUNCT_1,
      CARD_1, ORDINAL1, NUMBERS, CARD_3, MCART_1, WELLORD2, FINSET_1, SETFAM_1,
      DOMAIN_1, CONNSP_2, ZFMISC_1, STRUCT_0, OPENLATT, MEASURE1, PRE_TOPC,
      TOPS_1, TOPS_2, CONNSP_1, TDLAT_3, WAYBEL23, PROB_1, TOPMETR, CANTOR_1,
      ORDERS_4, TOPGEN_1, TOPGEN_3, PCOMPS_1;
 constructors MEASURE1, TOPS_1, CONNSP_1, COMPTS_1, TDLAT_3, TOPMETR, OPENLATT,
      WAYBEL23, TOPGEN_2, ORDERS_4, TOPGEN_1, TOPGEN_3, PCOMPS_1, XTUPLE_0,
      XFAMILY;
 registrations SUBSET_1, RELSET_1, FINSET_1, NUMBERS, CARD_1, MEASURE1,
      STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, TOPMETR, TOPREAL6, TOPGEN_2,
      TOPGEN_1, CARD_3, COMPTS_1, XTUPLE_0;
 requirements NUMERALS, BOOLE, SUBSET;


begin :: Preliminaries

definition
  let T be 1-sorted;
  func TotFam T -> Subset-Family of T equals
:: TOPGEN_4:def 1
  bool the carrier of T;
end;

theorem :: TOPGEN_4:1
  for T being set, F being Subset-Family of T holds F is countable
  iff COMPLEMENT F is countable;

registration
  cluster RAT -> countable;
end;

scheme :: TOPGEN_4:sch 1
 FraenCoun11 { P[set] } :
  { {n} where n is Element of RAT : P[n] } is countable;

theorem :: TOPGEN_4:2
  for T being non empty TopSpace, A being Subset of T holds Der A = { x
  where x is Point of T : x in Cl (A \ {x}) };

registration
  cluster finite -> second-countable for TopStruct;
end;

registration
  cluster REAL -> non countable;
end;

registration
  cluster non countable -> non finite for set;
  cluster non finite -> non trivial for set;
  cluster non countable non empty for set;
end;

reserve T for non empty TopSpace,
  A, B for Subset of T,
  F, G for Subset-Family of T;

theorem :: TOPGEN_4:3
  A is closed iff Der A c= A;

theorem :: TOPGEN_4:4
  for T being non empty TopStruct, B being Basis of T, V being
Subset of T st V is open & V <> {} ex W being Subset of T st W in B & W c= V &
  W <> {};

begin :: Regular Formalization: Separable Spaces
:: 1.3.7. Theorem

theorem :: TOPGEN_4:5
  density T c= weight T;

theorem :: TOPGEN_4:6
  T is separable iff ex A being Subset of T st A is dense countable;

:: 1.3.8. Corollary

theorem :: TOPGEN_4:7
  T is second-countable implies T is separable;

registration
  cluster second-countable -> separable for non empty TopSpace;
end;

:: Exercises

theorem :: TOPGEN_4:8 :: Exercise 1.3.A.
  for T being non empty TopSpace, A, B being Subset of T st A, B
  are_separated holds Fr (A \/ B) = Fr A \/ Fr B;

:: Exercise 1.3.B.

theorem :: TOPGEN_4:9 :: Ex. 1.3.B. a)
  F is locally_finite implies Fr union F c= union Fr F;

theorem :: TOPGEN_4:10  :: also for empty TopSpaces
  for T being discrete non empty TopSpace holds T is separable iff
  card [#]T c= omega;

theorem :: TOPGEN_4:11
  for T being discrete non empty TopSpace holds T is separable iff T is
  countable;

begin :: Families of Subsets Closed for Countable Unions and Complement

definition
  let T, F;
  attr F is all-open-containing means
:: TOPGEN_4:def 2

  for A being Subset of T st A is open holds A in F;
end;

definition
  let T, F;
  attr F is all-closed-containing means
:: TOPGEN_4:def 3

  for A being Subset of T st A is closed holds A in F;
end;

definition
  let T be set, F be Subset-Family of T;
  attr F is closed_for_countable_unions means
:: TOPGEN_4:def 4

  for G being countable Subset-Family of T st G c= F holds union G in F;
end;

registration
  let T be set;
  cluster -> closed_for_countable_unions for SigmaField of T;
end;

theorem :: TOPGEN_4:12
  for T being set, F being Subset-Family of T st F is
  closed_for_countable_unions holds {} in F;

registration
  let T be set;
  cluster closed_for_countable_unions -> non empty for Subset-Family of T;
end;

theorem :: TOPGEN_4:13
  for T being set, F being Subset-Family of T holds F is
  SigmaField of T iff F is compl-closed closed_for_countable_unions;

definition
  let T be set, F be Subset-Family of T;
  attr F is closed_for_countable_meets means
:: TOPGEN_4:def 5

  for G being countable Subset-Family of T st G c= F holds meet G in F;
end;

theorem :: TOPGEN_4:14
  for F being Subset-Family of T holds F is all-closed-containing
  compl-closed iff F is all-open-containing compl-closed;

theorem :: TOPGEN_4:15
  for T being set, F being Subset-Family of T st F is compl-closed holds
  F = COMPLEMENT F;

theorem :: TOPGEN_4:16
  for T being set, F, G being Subset-Family of T st F c= G & G is
  compl-closed holds COMPLEMENT F c= G;

theorem :: TOPGEN_4:17
  for T being set, F being Subset-Family of T holds F is
  closed_for_countable_meets compl-closed iff F is closed_for_countable_unions
  compl-closed;

registration
  let T;
  cluster all-open-containing compl-closed closed_for_countable_unions ->
    all-closed-containing closed_for_countable_meets for Subset-Family of T;
  cluster all-closed-containing compl-closed closed_for_countable_meets ->
    all-open-containing closed_for_countable_unions for Subset-Family of T;
end;

begin :: On the Families of Subsets

registration
  let T be set;
  let F be countable Subset-Family of T;
  cluster COMPLEMENT F -> countable;
end;

registration
  let T be TopSpace;
  cluster empty -> open closed for Subset-Family of T;
end;

registration
  let T be TopSpace;
  cluster countable open closed for Subset-Family of T;
end;

theorem :: TOPGEN_4:18
  for T being set holds {} is empty Subset-Family of T;

registration
  cluster empty -> countable for set;
end;

begin :: Collective Properties of Families

theorem :: TOPGEN_4:19
  F = { A } implies (A is open iff F is open);

theorem :: TOPGEN_4:20
  F = { A } implies (A is closed iff F is closed);

definition
  let T be set, F, G be Subset-Family of T;
  redefine func INTERSECTION (F,G) -> Subset-Family of T;
  redefine func UNION (F,G) -> Subset-Family of T;
end;

theorem :: TOPGEN_4:21
  F is closed & G is closed implies INTERSECTION (F,G) is closed;

theorem :: TOPGEN_4:22
  F is closed & G is closed implies UNION (F,G) is closed;

theorem :: TOPGEN_4:23
  F is open & G is open implies INTERSECTION (F,G) is open;

theorem :: TOPGEN_4:24
  F is open & G is open implies UNION (F,G) is open;

theorem :: TOPGEN_4:25
  for T being set, F, G being Subset-Family of T holds card
  INTERSECTION (F,G) c= card [:F,G:];

theorem :: TOPGEN_4:26
  for T being set, F, G being Subset-Family of T holds card UNION
  (F,G) c= card [:F,G:];

theorem :: TOPGEN_4:27
  for F, G being set holds union UNION (F,G) c= union F \/ union G;

theorem :: TOPGEN_4:28
  for F, G being set st F <> {} & G <> {} holds union F \/ union G
  = union UNION (F,G);

theorem :: TOPGEN_4:29
  for F being set holds UNION ({},F) = {};

theorem :: TOPGEN_4:30
  for F, G being set holds UNION (F, G) = {} implies F = {} or G = {};

theorem :: TOPGEN_4:31
  for F, G being set st INTERSECTION (F, G) = {} holds F = {} or G = {};

theorem :: TOPGEN_4:32
  for F, G being set holds meet UNION (F,G) c= meet F \/ meet G;

theorem :: TOPGEN_4:33
  for F, G being set st F <> {} & G <> {} holds meet UNION(F,G) = meet F
  \/ meet G;

theorem :: TOPGEN_4:34
  for F, G being set st F <> {} & G <> {} holds meet F /\ meet G =
  meet INTERSECTION(F,G);

begin :: F_sigma and G_delta Types of Subsets

definition
  let T be TopSpace, A be Subset of T;
  attr A is F_sigma means
:: TOPGEN_4:def 6

  ex F being closed countable Subset-Family of T st A = union F;
end;

definition
  let T be TopSpace, A be Subset of T;
  attr A is G_delta means
:: TOPGEN_4:def 7

  ex F being open countable Subset-Family of T st A = meet F;
end;

registration
  let T;
  cluster empty -> F_sigma G_delta for Subset of T;
end;

theorem :: TOPGEN_4:35
  [#]T is F_sigma;

theorem :: TOPGEN_4:36
  [#]T is G_delta;

registration
  let T;
  cluster [#]T -> F_sigma G_delta;
end;

theorem :: TOPGEN_4:37
  A is F_sigma implies A` is G_delta;

theorem :: TOPGEN_4:38
  A is G_delta implies A` is F_sigma;

theorem :: TOPGEN_4:39
  A is F_sigma & B is F_sigma implies A /\ B is F_sigma;

theorem :: TOPGEN_4:40
  A is F_sigma & B is F_sigma implies A \/ B is F_sigma;

theorem :: TOPGEN_4:41
  A is G_delta & B is G_delta implies A \/ B is G_delta;

theorem :: TOPGEN_4:42
  A is G_delta & B is G_delta implies A /\ B is G_delta;

theorem :: TOPGEN_4:43
  for A being Subset of T st A is closed holds A is F_sigma;

theorem :: TOPGEN_4:44
  for A being Subset of T st A is open holds A is G_delta;

theorem :: TOPGEN_4:45
  for A being Subset of R^1 st A = RAT holds A is F_sigma;

begin :: T_1/2 Topological Spaces

definition
  let T be TopSpace;
  attr T is T_1/2 means
:: TOPGEN_4:def 8

  for A being Subset of T holds Der A is closed;
end;

theorem :: TOPGEN_4:46
  for T being TopSpace st T is T_1 holds T is T_1/2;

theorem :: TOPGEN_4:47
  for T being non empty TopSpace st T is T_1/2 holds T is T_0;

registration
  cluster T_1/2 -> T_0 for TopSpace;
  cluster T_1 -> T_1/2 for TopSpace;
end;

begin :: Condensation Points
:: Page 77 - 1.7.11

definition
  let T, A;
  let x be Point of T;
  pred x is_a_condensation_point_of A means
:: TOPGEN_4:def 9

  for N being a_neighborhood of x holds N /\ A is not countable;
end;

reserve x for Point of T;

theorem :: TOPGEN_4:48
  x is_a_condensation_point_of A & A c= B implies x
  is_a_condensation_point_of B;

definition
  let T, A;
  func A^0 -> Subset of T means
:: TOPGEN_4:def 10

  for x being Point of T holds x in it iff x is_a_condensation_point_of A;
end;

theorem :: TOPGEN_4:49
  for p being Point of T st p is_a_condensation_point_of A holds p
  is_an_accumulation_point_of A;

theorem :: TOPGEN_4:50
  A^0 c= Der A;

theorem :: TOPGEN_4:51
  A^0 = Cl (A^0);

theorem :: TOPGEN_4:52
  A c= B implies A^0 c= B^0;

theorem :: TOPGEN_4:53
  x is_a_condensation_point_of A \/ B implies x
  is_a_condensation_point_of A or x is_a_condensation_point_of B;

theorem :: TOPGEN_4:54
  (A \/ B)^0 = (A^0) \/ (B^0);

theorem :: TOPGEN_4:55
  A is countable implies not ex x being Point of T st x
  is_a_condensation_point_of A;

theorem :: TOPGEN_4:56
  A is countable implies A^0 = {};

registration
  let T;
  let A be countable Subset of T;
  cluster A^0 -> empty;
end;

theorem :: TOPGEN_4:57
  T is second-countable implies ex B being Basis of T st B is countable;

registration
  cluster second-countable non empty for TopSpace;
end;

begin :: Borel Families of Subsets

registration
  let T;
  cluster TotFam T -> non empty all-open-containing compl-closed
    closed_for_countable_unions;
end;

theorem :: TOPGEN_4:58
  for T being set, A being SetSequence of T holds
  rng A is countable non empty Subset-Family of T;

theorem :: TOPGEN_4:59
  for F, G being Subset-Family of T st F is all-open-containing &
  F c= G holds G is all-open-containing;

theorem :: TOPGEN_4:60
  for F, G being Subset-Family of T st F is all-closed-containing & F c=
  G holds G is all-closed-containing;

definition
  let T be 1-sorted;
  mode SigmaField of T is SigmaField of the carrier of T;
end;

registration
  let T be non empty TopSpace;
  cluster compl-closed closed_for_countable_unions closed_for_countable_meets
    all-closed-containing all-open-containing for Subset-Family of T;
end;

theorem :: TOPGEN_4:61
  sigma TotFam T is all-open-containing compl-closed
  closed_for_countable_unions;

registration
  let T;
  cluster sigma TotFam T -> all-open-containing compl-closed
    closed_for_countable_unions;
end;

registration
  let T be non empty 1-sorted;
  cluster sigma-additive compl-closed closed_for_countable_unions non empty
    for Subset-Family of T;
end;

registration
  let T be non empty TopSpace;
  cluster -> closed_for_countable_unions for SigmaField of T;
end;

theorem :: TOPGEN_4:62
  for T being non empty TopSpace, F being Subset-Family of T st F is
  compl-closed closed_for_countable_unions holds F is SigmaField of T;

registration
  let T be non empty TopSpace;
  cluster all-open-containing for SigmaField of T;
end;

registration
  let T be non empty TopSpace;
  cluster Topology_of T -> open all-open-containing;
end;

theorem :: TOPGEN_4:63
  for X being Subset-Family of T ex Y being all-open-containing
  compl-closed closed_for_countable_unions Subset-Family of T st X c= Y & for Z
  be all-open-containing compl-closed closed_for_countable_unions Subset-Family
  of T st X c= Z holds Y c= Z;

definition
  let T;
  func BorelSets T -> all-open-containing compl-closed
  closed_for_countable_unions Subset-Family of T means
:: TOPGEN_4:def 11

  for G being
all-open-containing compl-closed closed_for_countable_unions Subset-Family of T
  holds it c= G;
end;

theorem :: TOPGEN_4:64
  for F being closed Subset-Family of T holds F c= BorelSets T;

theorem :: TOPGEN_4:65
  for F being open Subset-Family of T holds F c= BorelSets T;

theorem :: TOPGEN_4:66
  BorelSets T = sigma Topology_of T;

definition
  let T, A;
  attr A is Borel means
:: TOPGEN_4:def 12

  A in BorelSets T;
end;

registration
  let T;
  cluster F_sigma -> Borel for Subset of T;
end;

registration
  let T;
  cluster G_delta -> Borel for Subset of T;
end;