Top source

Module mathcomp.analysis.topology_theory.bool_topology

From HB Require Import structures.
From mathcomp Require Import boot order algebra all_classical.
From mathcomp Require Import reals topology_structure uniform_structure.
From mathcomp Require Import pseudometric_structure order_topology compact.
From mathcomp Require Import discrete_topology.


Unset SsrOldRewriteGoalsOrder.

Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

HB

---

Source code

.

instance

---

Source code

Definition

---

Source code

_

---

Source code

:=

---

Source code

hasNbhs

---

Source code

.Build bool principal_filter.

HB

---

Source code

.

instance

---

Source code

Definition

---

Source code

_

---

Source code

:=

---

Source code

Discrete_ofNbhs

---

Source code

.Build bool erefl.

HB

---

Source code

.

instance

---

Source code

Definition

---

Source code

_

---

Source code

:=

---

Source code

DiscreteUniform_ofNbhs

---

Source code

.Build bool.

Lemma

bool_compact

---

Source code

: compact [set: bool].

Proof.

by rewrite setT_bool; apply/compactU; exact: compact_set1. Qed.

Local Lemma

bool_nbhs_itv

---

Source code

(

b

---

Source code

: bool) :
  nbhs b = filter_from
    (fun

i

---

Source code

=> itv_open_ends i /\ b \in i)
    (fun

i

---

Source code

=> [set` i]).

Proof.

rewrite nbhs_principalE eqEsubset; split=> U; first last.
  by case => V [_ Vb] VU; apply/principal_filterP/VU; apply: Vb.
move/principal_filterP; case: b.
  move=> Ut; exists `]false, +oo[; first split => //.
  by move=> r /=; rewrite in_itv /=; case: r.
move=> Ut; exists `]-oo, true[; first split => //.
by move=> r /=; rewrite in_itv /=; case: r.
Qed.

HB

---

Source code

.

instance

---

Source code

Definition

---

Source code

_

---

Source code

:=

---

Source code

Order_isNbhs

---

Source code

.Build _ bool bool_nbhs_itv.

HB

---

Source code

.

instance

---

Source code

Definition

---

Source code

_

---

Source code

{R

---

Source code

:

---

Source code

numDomainType}

---

Source code

:=
  @DiscretePseudoMetric_ofUniform.Build R bool.