-
Lemma fconnect_cycle y :
fconnect f x y = (y \in p).
+
Lemma fconnect_cycle y :
fconnect f x y = (y \in p).
-
Lemma order_cycle :
order x = size p.
+
Lemma order_cycle :
order x = size p.
-
Lemma orbit_rot_cycle :
{i : nat | orbit x = rot i p}.
+
Lemma orbit_rot_cycle :
{i : nat | orbit x = rot i p}.
End Loop.
@@ -387,112 +386,113 @@
Section orbit_in.
-
Variable S :
pred_sort (
predPredType T).
+
Variable S :
{pred T}.
-
Hypothesis f_in :
{in S, ∀ x,
f x \in S}.
-
Hypothesis injf :
{in S &, injective f}.
+
Hypothesis f_in :
{in S, ∀ x,
f x \in S}.
+
Hypothesis injf :
{in S &, injective f}.
-
Lemma iter_in :
{in S, ∀ x i,
iter i f x \in S}.
+
Lemma iter_in :
{in S, ∀ x i,
iter i f x \in S}.
-
Lemma finv_in :
{in S, ∀ x,
finv x \in S}.
+
Lemma finv_in :
{in S, ∀ x,
finv x \in S}.
-
Lemma f_finv_in :
{in S, cancel finv f}.
+
Lemma f_finv_in :
{in S, cancel finv f}.
-
Lemma finv_f_in :
{in S, cancel f finv}.
+
Lemma finv_f_in :
{in S, cancel f finv}.
-
Lemma finv_inj_in :
{in S &, injective finv}.
+
Lemma finv_inj_in :
{in S &, injective finv}.
-
Lemma fconnect_sym_in :
{in S &, ∀ x y,
fconnect f x y = fconnect f y x}.
+
Lemma fconnect_sym_in :
{in S &, ∀ x y,
fconnect f x y = fconnect f y x}.
-
Lemma iter_order_in :
{in S, ∀ x,
iter (
order x)
f x = x}.
+
Lemma iter_order_in :
{in S, ∀ x,
iter (
order x)
f x = x}.
Lemma iter_finv_in n :
-
{in S, ∀ x,
n ≤ order x → iter n finv x = iter (
order x - n)
f x}.
+
{in S, ∀ x,
n ≤ order x → iter n finv x = iter (
order x - n)
f x}.
-
Lemma cycle_orbit_in :
{in S, ∀ x, (
fcycle f) (
orbit x)
}.
+
Lemma cycle_orbit_in :
{in S, ∀ x, (
fcycle f) (
orbit x)
}.
-
Lemma fpath_finv_in p x :
(x \in S) && (fpath finv x p) =
-
(last x p \in S) && (fpath f (
last x p) (
rev (
belast x p))
).
+
Lemma fpath_finv_in p x :
(x \in S) && (fpath finv x p) =
+
(last x p \in S) && (fpath f (
last x p) (
rev (
belast x p))
).
-
Lemma fpath_finv_f_in p :
{in S, ∀ x,
-
fpath finv x p → fpath f (
last x p) (
rev (
belast x p))
}.
+
Lemma fpath_finv_f_in p :
{in S, ∀ x,
+
fpath finv x p → fpath f (
last x p) (
rev (
belast x p))
}.
-
Lemma fpath_f_finv_in p x :
last x p \in S →
-
fpath f (
last x p) (
rev (
belast x p))
→ fpath finv x p.
+
Lemma fpath_f_finv_in p x :
last x p \in S →
+
fpath f (
last x p) (
rev (
belast x p))
→ fpath finv x p.
End orbit_in.
-
Hypothesis injf :
injective f.
+
Hypothesis injf :
injective f.
-
Lemma f_finv :
cancel finv f.
+
Lemma f_finv :
cancel finv f.
-
Lemma finv_f :
cancel f finv.
+
Lemma finv_f :
cancel f finv.
-
Lemma fin_inj_bij :
bijective f.
+
Lemma fin_inj_bij :
bijective f.
-
Lemma finv_bij :
bijective finv.
+
Lemma finv_bij :
bijective finv.
-
Lemma finv_inj :
injective finv.
+
Lemma finv_inj :
injective finv.
-
Lemma fconnect_sym x y :
fconnect f x y = fconnect f y x.
+
Lemma fconnect_sym x y :
fconnect f x y = fconnect f y x.
Let symf :=
fconnect_sym.
-
Lemma iter_order x :
iter (
order x)
f x = x.
+
Lemma iter_order x :
iter (
order x)
f x = x.
-
Lemma iter_finv n x :
n ≤ order x → iter n finv x = iter (
order x - n)
f x.
+
Lemma iter_finv n x :
n ≤ order x → iter n finv x = iter (
order x - n)
f x.
Lemma cycle_orbit x :
fcycle f (
orbit x).
-
Lemma fpath_finv x p :
fpath finv x p = fpath f (
last x p) (
rev (
belast x p)).
+
Lemma fpath_finv x p :
fpath finv x p = fpath f (
last x p) (
rev (
belast x p)).
-
Lemma same_fconnect_finv :
fconnect finv =2 fconnect f.
+
Lemma same_fconnect_finv :
fconnect finv =2 fconnect f.
-
Lemma fcard_finv :
fcard_mem finv =1 fcard_mem f.
+
Lemma fcard_finv :
fcard_mem finv =1 fcard_mem f.
-
Definition order_set n :
pred T :=
[pred x | order x == n].
+
Definition order_set n :
pred T :=
[pred x | order x == n].
-
Lemma fcard_order_set n (
a :
pred T) :
-
a \subset order_set n → fclosed f a → fcard f a × n = #|a|.
+
Lemma fcard_order_set n (
a :
{pred T}) :
+
a \subset order_set n → fclosed f a → fcard f a × n = #|a|.
-
Lemma fclosed1 (
a :
pred T) :
fclosed f a → ∀ x,
(x \in a) = (f x \in a).
+
Lemma fclosed1 (
a :
{pred T}) :
+
fclosed f a → ∀ x,
(x \in a) = (f x \in a).
-
Lemma same_fconnect1 x :
fconnect f x =1 fconnect f (
f x).
+
Lemma same_fconnect1 x :
fconnect f x =1 fconnect f (
f x).
-
Lemma same_fconnect1_r x y :
fconnect f x y = fconnect f x (
f y).
+
Lemma same_fconnect1_r x y :
fconnect f x y = fconnect f x (
f y).
End Orbit.
@@ -506,22 +506,22 @@
Variable T :
finType.
-
Lemma fconnect_id (
x :
T) :
fconnect id x =1 xpred1 x.
+
Lemma fconnect_id (
x :
T) :
fconnect id x =1 xpred1 x.
-
Lemma order_id (
x :
T) :
order id x = 1.
+
Lemma order_id (
x :
T) :
order id x = 1.
-
Lemma orbit_id (
x :
T) :
orbit id x = [:: x].
+
Lemma orbit_id (
x :
T) :
orbit id x = [:: x].
-
Lemma froots_id (
x :
T) :
froots id x.
+
Lemma froots_id (
x :
T) :
froots id x.
-
Lemma froot_id (
x :
T) :
froot id x = x.
+
Lemma froot_id (
x :
T) :
froot id x = x.
-
Lemma fcard_id (
a :
pred T) :
fcard id a = #|a|.
+
Lemma fcard_id (
a :
{pred T}) :
fcard id a = #|a|.
End FconnectId.
@@ -530,29 +530,29 @@
Section FconnectEq.
-
Variables (
T :
finType) (
f f' :
T → T).
+
Variables (
T :
finType) (
f f' :
T → T).
-
Lemma finv_eq_can :
cancel f f' → finv f =1 f'.
+
Lemma finv_eq_can :
cancel f f' → finv f =1 f'.
-
Hypothesis eq_f :
f =1 f'.
+
Hypothesis eq_f :
f =1 f'.
Let eq_rf :=
eq_frel eq_f.
-
Lemma eq_fconnect :
fconnect f =2 fconnect f'.
+
Lemma eq_fconnect :
fconnect f =2 fconnect f'.
-
Lemma eq_fcard :
fcard_mem f =1 fcard_mem f'.
+
Lemma eq_fcard :
fcard_mem f =1 fcard_mem f'.
-
Lemma eq_finv :
finv f =1 finv f'.
+
Lemma eq_finv :
finv f =1 finv f'.
-
Lemma eq_froot :
froot f =1 froot f'.
+
Lemma eq_froot :
froot f =1 froot f'.
-
Lemma eq_froots :
froots f =1 froots f'.
+
Lemma eq_froots :
froots f =1 froots f'.
End FconnectEq.
@@ -561,17 +561,17 @@
Section FinvEq.
-
Variables (
T :
finType) (
f :
T → T).
-
Hypothesis injf :
injective f.
+
Variables (
T :
finType) (
f :
T → T).
+
Hypothesis injf :
injective f.
-
Lemma finv_inv :
finv (
finv f)
=1 f.
+
Lemma finv_inv :
finv (
finv f)
=1 f.
-
Lemma order_finv :
order (
finv f)
=1 order f.
+
Lemma order_finv :
order (
finv f)
=1 order f.
-
Lemma order_set_finv n :
order_set (
finv f)
n =i order_set f n.
+
Lemma order_set_finv n :
order_set (
finv f)
n =i order_set f n.
End FinvEq.
@@ -580,58 +580,58 @@
Section RelAdjunction.
-
Variables (
T T' :
finType) (
h :
T' → T) (
e :
rel T) (
e' :
rel T').
+
Variables (
T T' :
finType) (
h :
T' → T) (
e :
rel T) (
e' :
rel T').
Hypotheses (
sym_e :
connect_sym e) (
sym_e' :
connect_sym e').
Record rel_adjunction_mem m_a :=
RelAdjunction {
-
rel_unit x :
in_mem x m_a → {x' : T' | connect e x (
h x')
};
+
rel_unit x :
in_mem x m_a → {x' : T' | connect e x (
h x')
};
rel_functor x' y' :
-
in_mem (
h x')
m_a → connect e' x' y' = connect e (
h x') (
h y')
+
in_mem (
h x')
m_a → connect e' x' y' = connect e (
h x') (
h y')
}.
-
Variable a :
pred T.
+
Variable a :
{pred T}.
Hypothesis cl_a :
closed e a.
-
Lemma intro_adjunction (
h' :
∀ x,
x \in a → T') :
-
(∀ x a_x,
-
[/\ connect e x (
h (
h' x a_x))
-
& ∀ y a_y,
e x y → connect e' (
h' x a_x) (
h' y a_y)
]) →
-
(∀ x' a_x,
-
[/\ connect e' x' (
h' (
h x')
a_x)
-
& ∀ y',
e' x' y' → connect e (
h x') (
h y')
]) →
+
Lemma intro_adjunction (
h' :
∀ x,
x \in a → T') :
+
(∀ x a_x,
+
[/\ connect e x (
h (
h' x a_x))
+
& ∀ y a_y,
e x y → connect e' (
h' x a_x) (
h' y a_y)
]) →
+
(∀ x' a_x,
+
[/\ connect e' x' (
h' (
h x')
a_x)
+
& ∀ y',
e' x' y' → connect e (
h x') (
h y')
]) →
rel_adjunction.
Lemma strict_adjunction :
-
injective h → a \subset codom h → rel_base h e e' [predC a] →
+
injective h → a \subset codom h → rel_base h e e' [predC a] →
rel_adjunction.
Let ccl_a :=
closed_connect cl_a.
-
Lemma adjunction_closed :
rel_adjunction → closed e' [preim h of a].
+
Lemma adjunction_closed :
rel_adjunction → closed e' [preim h of a].
Lemma adjunction_n_comp :
-
rel_adjunction → n_comp e a = n_comp e' [preim h of a].
+
rel_adjunction → n_comp e a = n_comp e' [preim h of a].
End RelAdjunction.
-
Notation rel_adjunction h e e' a := (
rel_adjunction_mem h e e' (
mem a)).
-
Notation "@ 'rel_adjunction' T T' h e e' a" :=
- (@
rel_adjunction_mem T T' h e e' (
mem a))
+
Notation rel_adjunction h e e' a := (
rel_adjunction_mem h e e' (
mem a)).
+
Notation "@ 'rel_adjunction' T T' h e e' a" :=
+ (@
rel_adjunction_mem T T' h e e' (
mem a))
(
at level 10,
T,
T',
h,
e,
e',
a at level 8,
only parsing) :
type_scope.
Notation fun_adjunction h f f' a := (
rel_adjunction h (
frel f) (
frel f')
a).
-
Notation "@ 'fun_adjunction' T T' h f f' a" :=
- (
@rel_adjunction T T' h (frel f) (frel f') a)
+
Notation "@ 'fun_adjunction' T T' h f f' a" :=
+ (
@rel_adjunction T T' h (frel f) (frel f') a)
(
at level 10,
T,
T',
h,
f,
f',
a at level 8,
only parsing) :
type_scope.
--
cgit v1.2.3