| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (735 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (27 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (64 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (283 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (55 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (32 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (30 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (222 entries) |
Global Index
A
ABapprox [inductive, in Continuity.BredeHerbelin.brede_herbelin]ABapprox_PtoT_pruning [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABapprox_pruning_TtoP [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABbarred [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_choicefun [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_barred_TtoP_size_inf [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_PtoT_barred [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_barred_TtoP [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABchoicefun [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABchoice_PtoT_choice [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABchoice_choice_TtoP [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABDownarborification [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABDownmonotonisation [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABDownmonot_monotone [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABDown_PtoT_P [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABis_tree [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABmonotone [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABmonotone_size [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABmonot_barred [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABUparborification [inductive, in Continuity.BredeHerbelin.brede_herbelin]
ABUparborification_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABUparborification_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation [inductive, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_size_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_size_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_size [inductive, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonot_monotone [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmono_size_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABUpsize_monotone_size [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABUp_Up_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₑ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₐ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[| _ |] (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↓⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↑⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇓⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
Additional_Lemmas.A [variable, in Continuity.BredeHerbelin.brede_herbelin]
Additional_Lemmas [section, in Continuity.BredeHerbelin.brede_herbelin]
Add_induction_step [lemma, in Continuity.BI]
Add_cat [lemma, in Continuity.BI]
Add_rcons [lemma, in Continuity.BI]
all_uniform [lemma, in Continuity.continuity_zoo_Prop]
approx [constructor, in Continuity.BredeHerbelin.brede_herbelin]
arbor_is_tree [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Ask [constructor, in Continuity.continuity_zoo_Prop]
ask [constructor, in Continuity.continuity_zoo_Prop]
B
BarInduction [section, in Continuity.BI]BarInduction.A [variable, in Continuity.BI]
BarInduction.dBI [variable, in Continuity.BI]
BarInduction.R [variable, in Continuity.BI]
barred [definition, in Continuity.extra_principles]
barred_ABbarred_PtoT_Up [lemma, in Continuity.BredeHerbelin.brede_herbelin]
barred_barred_Upmon [lemma, in Continuity.BredeHerbelin.brede_herbelin]
barred_ABbarred_PtoT [lemma, in Continuity.BredeHerbelin.brede_herbelin]
barred_TtoP_ABbarred [lemma, in Continuity.BredeHerbelin.brede_herbelin]
barred_Bseq_cont [lemma, in Continuity.BI]
barred_Bseq_cont_aux [lemma, in Continuity.BI]
Bars [section, in Continuity.extra_principles]
Bbeta [definition, in Continuity.continuity_zoo_Prop]
BbetaP [lemma, in Continuity.continuity_zoo_Prop]
Bbeta_dep [constructor, in Continuity.continuity_zoo_Prop]
Bcoind_dial_cont [definition, in Continuity.Brouwer_ext]
Bcoind_dial_cont_to_neigh_cont [lemma, in Continuity.kawai2018]
Bconst [constructor, in Continuity.kawai2018]
Bconst_at [constructor, in Continuity.kawai2018]
Beta [constructor, in Continuity.BredeHerbelin.brede_herbelin]
beta [constructor, in Continuity.continuity_zoo_Prop]
Beta_dep [constructor, in Continuity.continuity_zoo_Prop]
beval [definition, in Continuity.continuity_zoo_Prop]
Beval_ext_tree_monotone [lemma, in Continuity.Brouwer_ext]
Beval_ext_tree_output_unique [lemma, in Continuity.Brouwer_ext]
Beval_ext_tree_constant [lemma, in Continuity.Brouwer_ext]
Beval_ext_tree_map_aux [lemma, in Continuity.Brouwer_ext]
Beval_ext_tree_trace [definition, in Continuity.Brouwer_ext]
Beval_ext_tree_trace_aux [definition, in Continuity.Brouwer_ext]
Beval_ext_tree [definition, in Continuity.Brouwer_ext]
Beval_ext_tree_aux [definition, in Continuity.Brouwer_ext]
beval_list_modulus_at [lemma, in Continuity.BI]
beval_list_barred [lemma, in Continuity.BI]
beval_list_barred_aux [lemma, in Continuity.BI]
beval_list_mon [lemma, in Continuity.BI]
beval_list [definition, in Continuity.BI]
beval_ext [lemma, in Continuity.BI]
beval_trace [definition, in Continuity.BI]
Bext_tree [definition, in Continuity.Brouwer_ext]
BI [library]
Bieval [definition, in Continuity.Brouwer_ext]
Bieval_output_unique [lemma, in Continuity.Brouwer_ext]
Bieval_monotone_plus [lemma, in Continuity.Brouwer_ext]
Bieval_monotone [lemma, in Continuity.Brouwer_ext]
Bieval_trace_inf [lemma, in Continuity.kawai2018]
Bieval_trace_Some [lemma, in Continuity.kawai2018]
Bieval_trace [definition, in Continuity.kawai2018]
Bieval_pred_trace [lemma, in Continuity.BI]
Bieval_trace_spec [lemma, in Continuity.BI]
Bieval_trace [definition, in Continuity.BI]
Bieval_pred_to_Bitree_spec [lemma, in Continuity.BI]
BIProp11Down [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp11Down_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp11Up [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp11Up_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp12 [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp12Up [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp12Up_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp12_sym_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp12_sym [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp12_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp13 [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp13Down [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp13Down_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp13Up_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp13_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
bite [constructor, in Continuity.continuity_zoo_Prop]
Bitree [inductive, in Continuity.Brouwer_ext]
Bitree_cont_to_itree_cont [lemma, in Continuity.Brouwer_ext]
Bitree_to_itreeP [lemma, in Continuity.Brouwer_ext]
Bitree_to_itreeP_aux [lemma, in Continuity.Brouwer_ext]
Bitree_to_itree [definition, in Continuity.Brouwer_ext]
Bitree_to_itree_aux [definition, in Continuity.Brouwer_ext]
Bitree_to_option_Bieval [lemma, in Continuity.Brouwer_ext]
Bitree_to_option [definition, in Continuity.Brouwer_ext]
BI_GBI_alt [lemma, in Continuity.BredeHerbelin.brede_herbelin]
BI_alt [definition, in Continuity.BredeHerbelin.brede_herbelin]
BI_mon.A [variable, in Continuity.BredeHerbelin.brede_herbelin]
BI_mon [section, in Continuity.BredeHerbelin.brede_herbelin]
BI_GBI_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
BI_GBI [lemma, in Continuity.BredeHerbelin.brede_herbelin]
BI_ind [definition, in Continuity.extra_principles]
Bneigh_cont_equiv_dialogue_cont_Brouwer [lemma, in Continuity.kawai2018]
Bneigh_continuous_neigh_continuous [lemma, in Continuity.kawai2018]
Bneigh_cont [definition, in Continuity.kawai2018]
brede_herbelin [library]
Bret [constructor, in Continuity.Brouwer_ext]
Brouwer [abbreviation, in Continuity.continuity_zoo_Prop]
Brouwer [section, in Continuity.continuity_zoo_Prop]
Brouwer_interaction_trees.R [variable, in Continuity.Brouwer_ext]
Brouwer_interaction_trees.A [variable, in Continuity.Brouwer_ext]
Brouwer_interaction_trees [section, in Continuity.Brouwer_ext]
Brouwer_ext_tree.R [variable, in Continuity.Brouwer_ext]
Brouwer_ext_tree.A [variable, in Continuity.Brouwer_ext]
Brouwer_ext_tree [section, in Continuity.Brouwer_ext]
Brouwer_operation_at_Type_spec [lemma, in Continuity.kawai2018]
Brouwer_operation_at'_spec1 [lemma, in Continuity.kawai2018]
Brouwer_operation_at_Type_sind [definition, in Continuity.kawai2018]
Brouwer_operation_at_Type_rec [definition, in Continuity.kawai2018]
Brouwer_operation_at_Type_ind [definition, in Continuity.kawai2018]
Brouwer_operation_at_Type_rect [definition, in Continuity.kawai2018]
Brouwer_operation_at_Type [inductive, in Continuity.kawai2018]
Brouwer_operation_at'_sind [definition, in Continuity.kawai2018]
Brouwer_operation_at'_rec [definition, in Continuity.kawai2018]
Brouwer_operation_at'_ind [definition, in Continuity.kawai2018]
Brouwer_operation_at'_rect [definition, in Continuity.kawai2018]
Brouwer_operation_at' [inductive, in Continuity.kawai2018]
Brouwer_operation_at_spec [lemma, in Continuity.kawai2018]
Brouwer_operation_at_sind [definition, in Continuity.kawai2018]
Brouwer_operation_at_ind [definition, in Continuity.kawai2018]
Brouwer_operation_at [inductive, in Continuity.kawai2018]
Brouwer_operation_sind [definition, in Continuity.kawai2018]
Brouwer_operation_ind [definition, in Continuity.kawai2018]
Brouwer_operation [inductive, in Continuity.kawai2018]
Brouwer_ext [library]
Brouwer.A [variable, in Continuity.continuity_zoo_Prop]
Brouwer.R [variable, in Continuity.continuity_zoo_Prop]
Bseq_cont_to_dialogue_cont_Brouwer [lemma, in Continuity.BI]
Bsup [constructor, in Continuity.kawai2018]
Bsup_at_Type [constructor, in Continuity.kawai2018]
Bsup_at' [constructor, in Continuity.kawai2018]
Bsup_at [constructor, in Continuity.kawai2018]
Btree [inductive, in Continuity.continuity_zoo_Prop]
Btree_fun_cont_valid [definition, in Continuity.Brouwer_ext]
Btree_fun_cont [definition, in Continuity.Brouwer_ext]
Btree_to_dialogueP [lemma, in Continuity.continuity_zoo_Prop]
Btree_to_dialogueP_aux [lemma, in Continuity.continuity_zoo_Prop]
Btree_to_dialogue [definition, in Continuity.continuity_zoo_Prop]
Btree_to_dialogue_aux [definition, in Continuity.continuity_zoo_Prop]
Btree_dep_sind [definition, in Continuity.continuity_zoo_Prop]
Btree_dep_rec [definition, in Continuity.continuity_zoo_Prop]
Btree_dep_ind [definition, in Continuity.continuity_zoo_Prop]
Btree_dep_rect [definition, in Continuity.continuity_zoo_Prop]
Btree_dep [inductive, in Continuity.continuity_zoo_Prop]
Btree_sind [definition, in Continuity.continuity_zoo_Prop]
Btree_rec [definition, in Continuity.continuity_zoo_Prop]
Btree_ind [definition, in Continuity.continuity_zoo_Prop]
Btree_rect [definition, in Continuity.continuity_zoo_Prop]
Bvalid_every_list [lemma, in Continuity.Brouwer_ext]
Bvalid_plus [lemma, in Continuity.Brouwer_ext]
Bvalid_ext_tree [definition, in Continuity.Brouwer_ext]
Bvis [constructor, in Continuity.Brouwer_ext]
C
Cantor [section, in Continuity.continuity_zoo_Prop]cantor [lemma, in Continuity.BredeHerbelin.cantor]
cantor [library]
Cantor_Prop [lemma, in Continuity.BredeHerbelin.cantor]
Cantor.A [variable, in Continuity.continuity_zoo_Prop]
Cantor.fix_types.a0 [variable, in Continuity.continuity_zoo_Prop]
Cantor.fix_types.E [variable, in Continuity.continuity_zoo_Prop]
Cantor.fix_types.R [variable, in Continuity.continuity_zoo_Prop]
Cantor.fix_types.A [variable, in Continuity.continuity_zoo_Prop]
Cantor.fix_types.Q [variable, in Continuity.continuity_zoo_Prop]
Cantor.fix_types [section, in Continuity.continuity_zoo_Prop]
Cantor.L [variable, in Continuity.continuity_zoo_Prop]
Cantor.L_spec [variable, in Continuity.continuity_zoo_Prop]
Cantor.Q [variable, in Continuity.continuity_zoo_Prop]
Cantor.R [variable, in Continuity.continuity_zoo_Prop]
case_to_false [lemma, in Continuity.BredeHerbelin.cantor]
cBI_implies_CI_fail.cBI [variable, in Continuity.BI]
cBI_implies_CI_fail.R [variable, in Continuity.BI]
cBI_implies_CI_fail.A [variable, in Continuity.BI]
cBI_implies_CI_fail [section, in Continuity.BI]
choicefun [definition, in Continuity.BredeHerbelin.brede_herbelin]
choicefun_Downarbor_choicefun [lemma, in Continuity.BredeHerbelin.brede_herbelin]
choice_ABchoice_PtoT [lemma, in Continuity.BredeHerbelin.brede_herbelin]
choice_TtoP_ABchoice [lemma, in Continuity.BredeHerbelin.brede_herbelin]
CI_imp_c_BI [lemma, in Continuity.BI]
Classical [library]
CoCI_BI [lemma, in Continuity.BI]
coind_dial_cont_to_tree_fun_cont [lemma, in Continuity.continuity_zoo_Prop]
coind_dial_cont [definition, in Continuity.continuity_zoo_Prop]
comp_modulus_cont [definition, in Continuity.continuity_zoo_Prop]
Cont [definition, in Continuity.Classical]
continuity_principles.R [variable, in Continuity.continuity_zoo_Prop]
continuity_principles.A [variable, in Continuity.continuity_zoo_Prop]
continuity_principles.Q [variable, in Continuity.continuity_zoo_Prop]
continuity_principles [section, in Continuity.continuity_zoo_Prop]
continuity_zoo_Prop [library]
ContinuousBarInduction [section, in Continuity.BI]
ContinuousBarInduction.A [variable, in Continuity.BI]
ContinuousBarInduction.CI [variable, in Continuity.BI]
ContinuousBarInduction.R [variable, in Continuity.BI]
ContinuousInduction [section, in Continuity.BI]
ContinuousInduction.A [variable, in Continuity.BI]
ContinuousInduction.CI [variable, in Continuity.BI]
continuous_via_interrogations_iff [lemma, in Continuity.continuity_zoo_Prop]
continuous_modulus_cont_nat [definition, in Continuity.continuity_zoo_Prop]
continuous_modulus_cont [definition, in Continuity.continuity_zoo_Prop]
c_BI_imp_CI [lemma, in Continuity.BI]
c_BI [definition, in Continuity.BI]
c_bar [definition, in Continuity.BI]
D
DC [definition, in Continuity.BredeHerbelin.brede_herbelin]DCProp11 [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp11_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp12 [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp12_sym_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp12_sym [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp12_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp13 [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp13_sym_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp13_sym [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp13_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₑ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₐ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[| _ |] (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇓⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↓⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↑⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↓⁻ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇓⁻ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇑⁻ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
DC_GDC_BI_GBI.A [variable, in Continuity.BredeHerbelin.brede_herbelin]
DC_GDC_BI_GBI [section, in Continuity.BredeHerbelin.brede_herbelin]
decidable_iff [lemma, in Continuity.Util]
Delta0_choice [lemma, in Continuity.continuity_zoo_Prop]
deval [definition, in Continuity.continuity_zoo_Prop]
deval_list_to_dialogue_trace [definition, in Continuity.continuity_zoo_Prop]
dialogue [abbreviation, in Continuity.continuity_zoo_Prop]
dialogue [inductive, in Continuity.continuity_zoo_Prop]
dialogue_is_uniform [lemma, in Continuity.continuity_zoo_Prop]
dialogue_to_list [definition, in Continuity.continuity_zoo_Prop]
dialogue_not_uniform [lemma, in Continuity.continuity_zoo_Prop]
dialogue_F [lemma, in Continuity.continuity_zoo_Prop]
Dialogue_not_uniform [section, in Continuity.continuity_zoo_Prop]
dialogue_to_tree_fun_cont [lemma, in Continuity.continuity_zoo_Prop]
dialogue_to_ext_tree_for [lemma, in Continuity.continuity_zoo_Prop]
dialogue_to_ext_tree_wf [lemma, in Continuity.continuity_zoo_Prop]
dialogue_to_ext_tree [definition, in Continuity.continuity_zoo_Prop]
dialogue_to_btree_cont [lemma, in Continuity.continuity_zoo_Prop]
dialogue_to_BtreeP [lemma, in Continuity.continuity_zoo_Prop]
dialogue_to_Btree [definition, in Continuity.continuity_zoo_Prop]
dialogue_to_Brouwer [definition, in Continuity.continuity_zoo_Prop]
dialogue_cont_Brouwer_to_dialogue_cont [lemma, in Continuity.continuity_zoo_Prop]
dialogue_cont_to_is_dialogue [lemma, in Continuity.continuity_zoo_Prop]
dialogue_is_dialogue [lemma, in Continuity.continuity_zoo_Prop]
dialogue_cont_Brouwer [definition, in Continuity.continuity_zoo_Prop]
dialogue_cont [definition, in Continuity.continuity_zoo_Prop]
dialogue_sind [definition, in Continuity.continuity_zoo_Prop]
dialogue_rec [definition, in Continuity.continuity_zoo_Prop]
dialogue_ind [definition, in Continuity.continuity_zoo_Prop]
dialogue_rect [definition, in Continuity.continuity_zoo_Prop]
DNE [definition, in Continuity.Classical]
DNS [lemma, in Continuity.Classical]
DownABarbor_is_tree [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Downarborification [definition, in Continuity.BredeHerbelin.brede_herbelin]
Downarborification [definition, in Continuity.BredeHerbelin.minimal_example]
Downmonotonisation [definition, in Continuity.BredeHerbelin.brede_herbelin]
E
eq_catr [lemma, in Continuity.continuity_zoo_Prop]eq_catl [lemma, in Continuity.continuity_zoo_Prop]
eq_cat [lemma, in Continuity.continuity_zoo_Prop]
Eta [constructor, in Continuity.BredeHerbelin.brede_herbelin]
eta [constructor, in Continuity.continuity_zoo_Prop]
eval_ext_tree_pref_monotone [lemma, in Continuity.Brouwer_ext]
eval_ext_tree_pref_monotone_aux [lemma, in Continuity.Brouwer_ext]
eval_ext_tree_trace_from_pref [lemma, in Continuity.Brouwer_ext]
eval_ext_tree_from_pref [lemma, in Continuity.Brouwer_ext]
eval_list_map_In [lemma, in Continuity.BI]
eval_list_incl_none [lemma, in Continuity.BI]
eval_list_monotone [lemma, in Continuity.BI]
eval_list_notin_cat [lemma, in Continuity.BI]
eval_list_none_fun [lemma, in Continuity.BI]
eval_list_notin [lemma, in Continuity.BI]
eval_list_In_is_fun [lemma, in Continuity.BI]
eval_list_In [lemma, in Continuity.BI]
eval_list [definition, in Continuity.BI]
eval_modulus_to_ext [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_continuous [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_continuous [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_valid_eqtau [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_to_interrogation [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_size_eval_trace [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_size_eval [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_monotone [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_monotone [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_map [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_map_aux [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace [definition, in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_aux [definition, in Continuity.continuity_zoo_Prop]
eval_ext_tree_output_unique [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_constant [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_ext [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree [definition, in Continuity.continuity_zoo_Prop]
eval_ext_tree_aux [definition, in Continuity.continuity_zoo_Prop]
extra_principles [library]
extree_to_Bextree_noo_eq [lemma, in Continuity.Brouwer_ext]
extree_to_Bextree_noo [definition, in Continuity.Brouwer_ext]
extree_to_Bextree_spec [lemma, in Continuity.Brouwer_ext]
extree_to_Bextree [definition, in Continuity.Brouwer_ext]
extree_to_extree [definition, in Continuity.Brouwer_ext]
ext_tree_to_Bext_tree_valid [lemma, in Continuity.Brouwer_ext]
ext_tree_valid_eqtau_ask [lemma, in Continuity.continuity_zoo_Prop]
ext_tree_valid_valid [lemma, in Continuity.continuity_zoo_Prop]
ext_tree_valid [definition, in Continuity.continuity_zoo_Prop]
ext_tree_valid_aux [definition, in Continuity.continuity_zoo_Prop]
ext_tree_to_int_tree [definition, in Continuity.continuity_zoo_Prop]
ext_tree_for [definition, in Continuity.continuity_zoo_Prop]
ext_tree [definition, in Continuity.continuity_zoo_Prop]
ex_modulus_modulus_fun [lemma, in Continuity.continuity_zoo_Prop]
ex_modulus_cont_nat [definition, in Continuity.continuity_zoo_Prop]
ex_modulus_cont [definition, in Continuity.continuity_zoo_Prop]
F
F [definition, in Continuity.continuity_zoo_Prop]FinQuestion [section, in Continuity.continuity_zoo_Prop]
FinQuestion.A [variable, in Continuity.continuity_zoo_Prop]
FinQuestion.L [variable, in Continuity.continuity_zoo_Prop]
FinQuestion.L_spec [variable, in Continuity.continuity_zoo_Prop]
FinQuestion.Q [variable, in Continuity.continuity_zoo_Prop]
FinQuestion.R [variable, in Continuity.continuity_zoo_Prop]
fixed_magic_size [lemma, in Continuity.BredeHerbelin.brede_herbelin]
fixed_magic_incl [lemma, in Continuity.BredeHerbelin.brede_herbelin]
fixed_magic [definition, in Continuity.BredeHerbelin.brede_herbelin]
follow [definition, in Continuity.continuity_zoo_Prop]
followP [lemma, in Continuity.continuity_zoo_Prop]
from_pref_finite_equal [lemma, in Continuity.Brouwer_ext]
from_pref_map_iota [lemma, in Continuity.Brouwer_ext]
from_pref [definition, in Continuity.continuity_zoo_Prop]
G
GBI [definition, in Continuity.BredeHerbelin.brede_herbelin]GBI_BI_alt [lemma, in Continuity.BredeHerbelin.brede_herbelin]
GBI_inconsistent [lemma, in Continuity.BredeHerbelin.brede_herbelin]
GBI_monot_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
GBI_BI_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
GBI_dec.Magic.X [variable, in Continuity.BredeHerbelin.brede_herbelin]
GBI_dec.Magic [section, in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺s _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₑ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₐ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[| _ |] (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↓⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↑⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇓⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
GBI_dec.A [variable, in Continuity.BredeHerbelin.brede_herbelin]
GBI_dec [section, in Continuity.BredeHerbelin.brede_herbelin]
GBI_monot [lemma, in Continuity.BredeHerbelin.brede_herbelin]
GBI_GCI [lemma, in Continuity.BI]
GBI_GCI_Fail [lemma, in Continuity.BI]
GDC [definition, in Continuity.BredeHerbelin.brede_herbelin]
GDC_inconsistent [lemma, in Continuity.BredeHerbelin.brede_herbelin]
GDC_gen [section, in Continuity.BredeHerbelin.brede_herbelin]
GDC_tree [lemma, in Continuity.BredeHerbelin.brede_herbelin]
⇓⁻ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇑⁻ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
GDC_GBI_Definition.A [variable, in Continuity.BredeHerbelin.brede_herbelin]
GDC_GBI_Definition.Q [variable, in Continuity.BredeHerbelin.brede_herbelin]
GDC_GBI_Definition [section, in Continuity.BredeHerbelin.brede_herbelin]
GeneralisedBarInduction [section, in Continuity.BI]
GeneralisedBarInduction.A [variable, in Continuity.BI]
GeneralisedBarInduction.HGBI [variable, in Continuity.BI]
GeneralisedBarInduction.Q [variable, in Continuity.BI]
GeneralisedBarInduction.R [variable, in Continuity.BI]
H
hereditary_closure_rect [lemma, in Continuity.extra_principles]hereditary_closure_Acc [lemma, in Continuity.extra_principles]
hereditary_closure_sind [definition, in Continuity.extra_principles]
hereditary_closure_ind [definition, in Continuity.extra_principles]
hereditary_sons [constructor, in Continuity.extra_principles]
hereditary_self [constructor, in Continuity.extra_principles]
hereditary_closure [inductive, in Continuity.extra_principles]
hereditary_closure_sind [definition, in Continuity.BredeHerbelin.minimal_example]
hereditary_closure_rec [definition, in Continuity.BredeHerbelin.minimal_example]
hereditary_closure_ind [definition, in Continuity.BredeHerbelin.minimal_example]
hereditary_closure_rect [definition, in Continuity.BredeHerbelin.minimal_example]
hereditary_sons [constructor, in Continuity.BredeHerbelin.minimal_example]
hereditary_self [constructor, in Continuity.BredeHerbelin.minimal_example]
hereditary_closure [inductive, in Continuity.BredeHerbelin.minimal_example]
hered_mon_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
hered_mon_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
hered_mon [inductive, in Continuity.BredeHerbelin.brede_herbelin]
hered_Upmon_hered_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
hered_Upmon_hered [lemma, in Continuity.BredeHerbelin.brede_herbelin]
I
ibeta [constructor, in Continuity.BredeHerbelin.brede_herbelin]ieta [constructor, in Continuity.BredeHerbelin.brede_herbelin]
ieval [definition, in Continuity.continuity_zoo_Prop]
ieval_finapp_one_step_fuel [lemma, in Continuity.BI]
ieval_finapp_trace [lemma, in Continuity.BI]
ieval_trace [definition, in Continuity.BI]
ieval_finapp_monotone_ask_list_nomorefuel [lemma, in Continuity.BI]
ieval_finapp_monotone_ask_fuel [lemma, in Continuity.BI]
ieval_finapp_monotone_ask_list [lemma, in Continuity.BI]
ieval_finapp_monotone_output_fuel [lemma, in Continuity.BI]
ieval_finapp_monotone_output_list [lemma, in Continuity.BI]
ieval_finapp [definition, in Continuity.BI]
ieval_output_unique [lemma, in Continuity.continuity_zoo_Prop]
inclP [lemma, in Continuity.Util]
included_size [lemma, in Continuity.BredeHerbelin.brede_herbelin]
incl_iota_max [lemma, in Continuity.BredeHerbelin.brede_herbelin]
inconsistent [lemma, in Continuity.Classical]
indbarred [inductive, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_inductively_barred_dual [lemma, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_inductively_barred_Down_dual [lemma, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_inductively_barred [lemma, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_spec_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_spec_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_spec [inductive, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_fun_list_itree_indbarredP [lemma, in Continuity.BI]
indbarred_fun_list_itree_indbarredP_aux [lemma, in Continuity.BI]
inductively_barred_indbarred_dual [lemma, in Continuity.BredeHerbelin.brede_herbelin]
inductively_barred_indbarred_Down_dual [lemma, in Continuity.BredeHerbelin.brede_herbelin]
inductively_barred_indbarred [lemma, in Continuity.BredeHerbelin.brede_herbelin]
inductively_barred [definition, in Continuity.extra_principles]
InP [lemma, in Continuity.Util]
Intensional_Dialogue.funext [variable, in Continuity.continuity_zoo_Prop]
Intensional_Dialogue.R [variable, in Continuity.continuity_zoo_Prop]
Intensional_Dialogue.A [variable, in Continuity.continuity_zoo_Prop]
Intensional_Dialogue.Q [variable, in Continuity.continuity_zoo_Prop]
Intensional_Dialogue [section, in Continuity.continuity_zoo_Prop]
interrogation [inductive, in Continuity.continuity_zoo_Prop]
interrogation_equiv_eval_ext_tree [lemma, in Continuity.continuity_zoo_Prop]
interrogation_app [lemma, in Continuity.continuity_zoo_Prop]
interrogation_ext [lemma, in Continuity.continuity_zoo_Prop]
interrogation_cons [lemma, in Continuity.continuity_zoo_Prop]
interrogation_plus [lemma, in Continuity.continuity_zoo_Prop]
interrogation_sind [definition, in Continuity.continuity_zoo_Prop]
interrogation_ind [definition, in Continuity.continuity_zoo_Prop]
int_tree_to_ext_tree_one_step [lemma, in Continuity.continuity_zoo_Prop]
int_tree_to_ext_tree [definition, in Continuity.continuity_zoo_Prop]
int_dialogue_cont_to_dialogue_cont [lemma, in Continuity.continuity_zoo_Prop]
int_dialogue_cont [definition, in Continuity.continuity_zoo_Prop]
inverse [constructor, in Continuity.BredeHerbelin.cantor]
inversion_ask [lemma, in Continuity.continuity_zoo_Prop]
in_iota [lemma, in Continuity.BredeHerbelin.brede_herbelin]
in_map [lemma, in Continuity.BredeHerbelin.brede_herbelin]
In_eval_list [lemma, in Continuity.BI]
iota_rcons [lemma, in Continuity.Util]
is_tree [definition, in Continuity.BredeHerbelin.brede_herbelin]
is_fun_rcons_notin_dom [lemma, in Continuity.BI]
is_fun_cons_notin_dom [lemma, in Continuity.BI]
is_fun_cat_notin_dom [lemma, in Continuity.BI]
is_fun_list_incl [lemma, in Continuity.BI]
is_fun_map [lemma, in Continuity.BI]
is_fun_list [definition, in Continuity.BI]
is_dialogue_to_dialogue [lemma, in Continuity.continuity_zoo_Prop]
is_dialogue_to_dialogue_ext [lemma, in Continuity.continuity_zoo_Prop]
is_dialogue_sind [definition, in Continuity.continuity_zoo_Prop]
is_dialogue_rec [definition, in Continuity.continuity_zoo_Prop]
is_dialogue_ind [definition, in Continuity.continuity_zoo_Prop]
is_dialogue_rect [definition, in Continuity.continuity_zoo_Prop]
is_dialogue [inductive, in Continuity.continuity_zoo_Prop]
itree [abbreviation, in Continuity.Brouwer_ext]
Itree [abbreviation, in Continuity.BI]
Itree [inductive, in Continuity.continuity_zoo_Prop]
itree [inductive, in Continuity.continuity_zoo_Prop]
itree_to_Bitree_cont [lemma, in Continuity.Brouwer_ext]
itree_to_BitreeP [lemma, in Continuity.Brouwer_ext]
itree_to_Bitree_seq [lemma, in Continuity.Brouwer_ext]
itree_to_Bitree [definition, in Continuity.Brouwer_ext]
itree_indbarredP_change_fuel [lemma, in Continuity.BI]
itree_indbarredP_monotone [lemma, in Continuity.BI]
itree_indbarred_spec [lemma, in Continuity.BI]
itree_indbarredP_ind [lemma, in Continuity.BI]
itree_indbarredP_rect [definition, in Continuity.BI]
itree_in [constructor, in Continuity.BI]
itree_indbarredP [inductive, in Continuity.BI]
itree_indbarred_dialogue [lemma, in Continuity.BI]
itree_indbarred_dialogue_aux [lemma, in Continuity.BI]
itree_indbarred_sind [definition, in Continuity.BI]
itree_indbarred_rec [definition, in Continuity.BI]
itree_indbarred_ind [definition, in Continuity.BI]
itree_indbarred_rect [definition, in Continuity.BI]
itree_beta [constructor, in Continuity.BI]
itree_succ [constructor, in Continuity.BI]
itree_eta [constructor, in Continuity.BI]
itree_indbarred [inductive, in Continuity.BI]
K
Kawai [section, in Continuity.kawai2018]Kawai.A [variable, in Continuity.kawai2018]
Kawai.R [variable, in Continuity.kawai2018]
kawai2018 [library]
K0K [lemma, in Continuity.kawai2018]
K0K_aux [lemma, in Continuity.kawai2018]
L
list_to_dialogue_eq [lemma, in Continuity.continuity_zoo_Prop]list_to_dialogue_deval_eq [lemma, in Continuity.continuity_zoo_Prop]
list_to_cantor_swap [lemma, in Continuity.continuity_zoo_Prop]
list_to_dialogue [definition, in Continuity.continuity_zoo_Prop]
list_to_cantor [definition, in Continuity.continuity_zoo_Prop]
M
map_incl [lemma, in Continuity.BredeHerbelin.brede_herbelin]mem_fixed_magic [lemma, in Continuity.BredeHerbelin.brede_herbelin]
MinEx [section, in Continuity.BredeHerbelin.minimal_example]
MinEx.B [variable, in Continuity.BredeHerbelin.minimal_example]
minimal_example [library]
Modulus [section, in Continuity.continuity_zoo_Prop]
modulus [definition, in Continuity.continuity_zoo_Prop]
modulus_to_ext_tree [definition, in Continuity.continuity_zoo_Prop]
modulus_at_nat_to_modulus_at [lemma, in Continuity.continuity_zoo_Prop]
modulus_at_to_modulus_at_nat [lemma, in Continuity.continuity_zoo_Prop]
modulus_ex_modulus [lemma, in Continuity.continuity_zoo_Prop]
modulus_nat [definition, in Continuity.continuity_zoo_Prop]
modulus_at_nat [definition, in Continuity.continuity_zoo_Prop]
modulus_at [definition, in Continuity.continuity_zoo_Prop]
Modulus.A [variable, in Continuity.continuity_zoo_Prop]
Modulus.Q [variable, in Continuity.continuity_zoo_Prop]
Modulus.R [variable, in Continuity.continuity_zoo_Prop]
mon [constructor, in Continuity.BredeHerbelin.brede_herbelin]
mon [constructor, in Continuity.BredeHerbelin.minimal_example]
monotone [definition, in Continuity.BredeHerbelin.brede_herbelin]
monotone_ABUp_PtoT_P [lemma, in Continuity.BredeHerbelin.brede_herbelin]
monot_barred [lemma, in Continuity.BredeHerbelin.brede_herbelin]
MP [lemma, in Continuity.Classical]
N
nat_queries.R [variable, in Continuity.continuity_zoo_Prop]nat_queries.A [variable, in Continuity.continuity_zoo_Prop]
nat_queries [section, in Continuity.continuity_zoo_Prop]
neighborhoodfunction [definition, in Continuity.kawai2018]
neighborhood_wf_valid_Bext_tree [lemma, in Continuity.kawai2018]
neigh_cont_iff_Bcoind_dial_cont [lemma, in Continuity.kawai2018]
neigh_cont_to_Bcoind_dial_cont [lemma, in Continuity.kawai2018]
neigh_to_Bitree [definition, in Continuity.kawai2018]
neigh_cont_Btree_fun_cont [lemma, in Continuity.kawai2018]
neigh_realises_Beval [lemma, in Continuity.kawai2018]
neigh_realises_Beval_aux [lemma, in Continuity.kawai2018]
neigh_cont [definition, in Continuity.kawai2018]
neigh_realises [definition, in Continuity.kawai2018]
NoDupP [lemma, in Continuity.Util]
NoQuestions [constructor, in Continuity.continuity_zoo_Prop]
normask [constructor, in Continuity.continuity_zoo_Prop]
normret [constructor, in Continuity.continuity_zoo_Prop]
normsucccons [constructor, in Continuity.continuity_zoo_Prop]
normsuccnil [constructor, in Continuity.continuity_zoo_Prop]
normzerocons [constructor, in Continuity.continuity_zoo_Prop]
normzeronil [constructor, in Continuity.continuity_zoo_Prop]
norm1 [inductive, in Continuity.continuity_zoo_Prop]
norm1_sind [definition, in Continuity.continuity_zoo_Prop]
norm1_rec [definition, in Continuity.continuity_zoo_Prop]
norm1_ind [definition, in Continuity.continuity_zoo_Prop]
norm1_rect [definition, in Continuity.continuity_zoo_Prop]
norm2 [inductive, in Continuity.continuity_zoo_Prop]
norm2_sind [definition, in Continuity.continuity_zoo_Prop]
norm2_rec [definition, in Continuity.continuity_zoo_Prop]
norm2_ind [definition, in Continuity.continuity_zoo_Prop]
norm2_rect [definition, in Continuity.continuity_zoo_Prop]
Notallin [lemma, in Continuity.Util]
nth_nth' [lemma, in Continuity.BI]
nth' [definition, in Continuity.BI]
n_comp_n_plus [lemma, in Continuity.continuity_zoo_Prop]
n_comp [definition, in Continuity.continuity_zoo_Prop]
O
ord [definition, in Continuity.BredeHerbelin.brede_herbelin]Ord [section, in Continuity.BredeHerbelin.brede_herbelin]
ordP [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_iota_aux [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_map_aux [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_inf_size [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_inf_size_aux [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_incl' [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_NoDup [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_in_2 [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_sizeu_notin [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_notin [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_incl [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_nth_in [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_in [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_nth [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_rcons [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_size [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_drop [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_take [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_cat [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_inj [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_map_snd [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_aux [definition, in Continuity.BredeHerbelin.brede_herbelin]
Ord.A [variable, in Continuity.BredeHerbelin.brede_herbelin]
output [constructor, in Continuity.continuity_zoo_Prop]
P
padded_prefix [definition, in Continuity.continuity_zoo_Prop]padded_seq [definition, in Continuity.continuity_zoo_Prop]
pred_to_fun [definition, in Continuity.BI]
pred_to_Bitree_aux [definition, in Continuity.BI]
pref [definition, in Continuity.continuity_zoo_Prop]
prefix [definition, in Continuity.extra_principles]
pref_a_Bieval [lemma, in Continuity.BI]
pref_a_beval [lemma, in Continuity.BI]
pref_a_alpha [lemma, in Continuity.BI]
pref_a_eq [lemma, in Continuity.BI]
pref_a [definition, in Continuity.BI]
pref_padded_prefix [lemma, in Continuity.continuity_zoo_Prop]
pref_le_eq [lemma, in Continuity.continuity_zoo_Prop]
prune [constructor, in Continuity.BredeHerbelin.brede_herbelin]
prune [constructor, in Continuity.BredeHerbelin.minimal_example]
pruning [inductive, in Continuity.BredeHerbelin.brede_herbelin]
pruning [inductive, in Continuity.BredeHerbelin.minimal_example]
pruning_pruning_Downarbor [lemma, in Continuity.BredeHerbelin.brede_herbelin]
pruning_ABapprox_PtoT [lemma, in Continuity.BredeHerbelin.brede_herbelin]
pruning_TtoP_ABapprox [lemma, in Continuity.BredeHerbelin.brede_herbelin]
pruning_cat [lemma, in Continuity.BredeHerbelin.brede_herbelin]
pruning_arbor [lemma, in Continuity.BredeHerbelin.minimal_example]
ptot [constructor, in Continuity.BredeHerbelin.brede_herbelin]
PtoT [inductive, in Continuity.BredeHerbelin.brede_herbelin]
PtoT_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
PtoT_TtoP_ret [lemma, in Continuity.BredeHerbelin.brede_herbelin]
PtoT_TtoP_inv [lemma, in Continuity.BredeHerbelin.brede_herbelin]
PtoT_dual [definition, in Continuity.BredeHerbelin.brede_herbelin]
PtoT_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
PtoT_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
P_ABUp_PtoTB [lemma, in Continuity.BredeHerbelin.brede_herbelin]
P_ABDown_PtoT [lemma, in Continuity.BredeHerbelin.brede_herbelin]
P_Uparbor_PtoT [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Q
Q [abbreviation, in Continuity.Brouwer_ext]Q [abbreviation, in Continuity.Brouwer_ext]
Q [abbreviation, in Continuity.BI]
Q [abbreviation, in Continuity.BI]
Q [abbreviation, in Continuity.continuity_zoo_Prop]
Q [abbreviation, in Continuity.continuity_zoo_Prop]
Q [abbreviation, in Continuity.continuity_zoo_Prop]
R
R [abbreviation, in Continuity.BI]reflect1 [definition, in Continuity.continuity_zoo_Prop]
reflect2 [definition, in Continuity.continuity_zoo_Prop]
reify [lemma, in Continuity.continuity_zoo_Prop]
reify2 [lemma, in Continuity.continuity_zoo_Prop]
result [inductive, in Continuity.continuity_zoo_Prop]
result_sind [definition, in Continuity.continuity_zoo_Prop]
result_rec [definition, in Continuity.continuity_zoo_Prop]
result_ind [definition, in Continuity.continuity_zoo_Prop]
result_rect [definition, in Continuity.continuity_zoo_Prop]
ret [constructor, in Continuity.continuity_zoo_Prop]
Ret [constructor, in Continuity.continuity_zoo_Prop]
retraction_Lawvere [lemma, in Continuity.BredeHerbelin.cantor]
retract_of [definition, in Continuity.Classical]
right_invertible_sind [definition, in Continuity.BredeHerbelin.cantor]
right_invertible_ind [definition, in Continuity.BredeHerbelin.cantor]
right_invertible [inductive, in Continuity.BredeHerbelin.cantor]
S
sec [section, in Continuity.continuity_zoo_Prop]sec.A [variable, in Continuity.continuity_zoo_Prop]
sec.R [variable, in Continuity.continuity_zoo_Prop]
sefl_mon [constructor, in Continuity.BredeHerbelin.brede_herbelin]
self_modulus_tree_fun_cont [lemma, in Continuity.continuity_zoo_Prop]
self_modulus_cont [definition, in Continuity.continuity_zoo_Prop]
size_ord [lemma, in Continuity.BredeHerbelin.brede_herbelin]
sons_mon [constructor, in Continuity.BredeHerbelin.brede_herbelin]
spit [constructor, in Continuity.continuity_zoo_Prop]
T
Tarbor [constructor, in Continuity.BredeHerbelin.brede_herbelin]Tau [constructor, in Continuity.continuity_zoo_Prop]
tbeta [constructor, in Continuity.continuity_zoo_Prop]
Technical [section, in Continuity.BredeHerbelin.brede_herbelin]
test [lemma, in Continuity.BredeHerbelin.minimal_example]
teta [constructor, in Continuity.continuity_zoo_Prop]
Theorem5 [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Theorem5rev [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Tmon [constructor, in Continuity.BredeHerbelin.brede_herbelin]
Tmon_size [constructor, in Continuity.BredeHerbelin.brede_herbelin]
top [definition, in Continuity.BredeHerbelin.brede_herbelin]
top_cons [lemma, in Continuity.BredeHerbelin.brede_herbelin]
TreeFunction [section, in Continuity.continuity_zoo_Prop]
TreeFunction.A [variable, in Continuity.continuity_zoo_Prop]
TreeFunction.Q [variable, in Continuity.continuity_zoo_Prop]
TreeFunction.R [variable, in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_Brouwer [lemma, in Continuity.Brouwer_ext]
tree_fun_cont_to_Brouwer_aux [lemma, in Continuity.Brouwer_ext]
tree_fun_cont_equiv_self_modulus_cont [lemma, in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_self_modulus_cont [lemma, in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_tree_fun_cont_valid [lemma, in Continuity.continuity_zoo_Prop]
tree_fun_cont_iff_coind_dial_cont [lemma, in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_coind_dial_cont [lemma, in Continuity.continuity_zoo_Prop]
tree_fun_cont_wf_to_tree_fun_cont [lemma, in Continuity.continuity_zoo_Prop]
tree_fun_cont_valid [definition, in Continuity.continuity_zoo_Prop]
tree_fun_cont_wf [definition, in Continuity.continuity_zoo_Prop]
tree_fun_cont_via_interrogations [definition, in Continuity.continuity_zoo_Prop]
tree_fun_cont [definition, in Continuity.continuity_zoo_Prop]
TtoP [definition, in Continuity.BredeHerbelin.brede_herbelin]
TtoP_PtoT_inv [lemma, in Continuity.BredeHerbelin.brede_herbelin]
TtoP_PtoT_ret [definition, in Continuity.BredeHerbelin.brede_herbelin]
T14 [lemma, in Continuity.continuity_zoo_Prop]
T41 [lemma, in Continuity.continuity_zoo_Prop]
U
uniform_is_dialogue [lemma, in Continuity.continuity_zoo_Prop]uni_cont [definition, in Continuity.continuity_zoo_Prop]
unzip1_ord [lemma, in Continuity.BredeHerbelin.brede_herbelin]
unzip2_ord [lemma, in Continuity.BredeHerbelin.brede_herbelin]
UpABarbor_is_tree [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Uparbor_PtoT_P [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation [inductive, in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation [inductive, in Continuity.BredeHerbelin.minimal_example]
UpmonotonisationP [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation_sind [definition, in Continuity.BredeHerbelin.minimal_example]
Upmonotonisation_rec [definition, in Continuity.BredeHerbelin.minimal_example]
Upmonotonisation_ind [definition, in Continuity.BredeHerbelin.minimal_example]
Upmonotonisation_rect [definition, in Continuity.BredeHerbelin.minimal_example]
Upmonot_monotone [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Upmono_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
upP [lemma, in Continuity.BredeHerbelin.brede_herbelin]
useless_hypothesis [lemma, in Continuity.kawai2018]
Util [library]
V
valid_cat [lemma, in Continuity.continuity_zoo_Prop]valid_ext_tree [definition, in Continuity.continuity_zoo_Prop]
vis [constructor, in Continuity.continuity_zoo_Prop]
Vis [constructor, in Continuity.continuity_zoo_Prop]
W
wf_Bext_tree [definition, in Continuity.Brouwer_ext]wf_ext_tree [definition, in Continuity.continuity_zoo_Prop]
Notation Index
A
[ _ ]ₑ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin][ _ ]ₐ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
[| _ |] (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↓⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↑⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇓⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
D
[ _ ]ₑ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin][ _ ]ₐ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
[| _ |] (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇓⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↓⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↑⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↓⁻ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇓⁻ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇑⁻ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
G
⇑⁺s _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin][ _ ]ₑ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₐ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
[| _ |] (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↓⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↑⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇓⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇓⁻ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇑⁻ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
Variable Index
A
Additional_Lemmas.A [in Continuity.BredeHerbelin.brede_herbelin]B
BarInduction.A [in Continuity.BI]BarInduction.dBI [in Continuity.BI]
BarInduction.R [in Continuity.BI]
BI_mon.A [in Continuity.BredeHerbelin.brede_herbelin]
Brouwer_interaction_trees.R [in Continuity.Brouwer_ext]
Brouwer_interaction_trees.A [in Continuity.Brouwer_ext]
Brouwer_ext_tree.R [in Continuity.Brouwer_ext]
Brouwer_ext_tree.A [in Continuity.Brouwer_ext]
Brouwer.A [in Continuity.continuity_zoo_Prop]
Brouwer.R [in Continuity.continuity_zoo_Prop]
C
Cantor.A [in Continuity.continuity_zoo_Prop]Cantor.fix_types.a0 [in Continuity.continuity_zoo_Prop]
Cantor.fix_types.E [in Continuity.continuity_zoo_Prop]
Cantor.fix_types.R [in Continuity.continuity_zoo_Prop]
Cantor.fix_types.A [in Continuity.continuity_zoo_Prop]
Cantor.fix_types.Q [in Continuity.continuity_zoo_Prop]
Cantor.L [in Continuity.continuity_zoo_Prop]
Cantor.L_spec [in Continuity.continuity_zoo_Prop]
Cantor.Q [in Continuity.continuity_zoo_Prop]
Cantor.R [in Continuity.continuity_zoo_Prop]
cBI_implies_CI_fail.cBI [in Continuity.BI]
cBI_implies_CI_fail.R [in Continuity.BI]
cBI_implies_CI_fail.A [in Continuity.BI]
continuity_principles.R [in Continuity.continuity_zoo_Prop]
continuity_principles.A [in Continuity.continuity_zoo_Prop]
continuity_principles.Q [in Continuity.continuity_zoo_Prop]
ContinuousBarInduction.A [in Continuity.BI]
ContinuousBarInduction.CI [in Continuity.BI]
ContinuousBarInduction.R [in Continuity.BI]
ContinuousInduction.A [in Continuity.BI]
ContinuousInduction.CI [in Continuity.BI]
D
DC_GDC_BI_GBI.A [in Continuity.BredeHerbelin.brede_herbelin]F
FinQuestion.A [in Continuity.continuity_zoo_Prop]FinQuestion.L [in Continuity.continuity_zoo_Prop]
FinQuestion.L_spec [in Continuity.continuity_zoo_Prop]
FinQuestion.Q [in Continuity.continuity_zoo_Prop]
FinQuestion.R [in Continuity.continuity_zoo_Prop]
G
GBI_dec.Magic.X [in Continuity.BredeHerbelin.brede_herbelin]GBI_dec.A [in Continuity.BredeHerbelin.brede_herbelin]
GDC_GBI_Definition.A [in Continuity.BredeHerbelin.brede_herbelin]
GDC_GBI_Definition.Q [in Continuity.BredeHerbelin.brede_herbelin]
GeneralisedBarInduction.A [in Continuity.BI]
GeneralisedBarInduction.HGBI [in Continuity.BI]
GeneralisedBarInduction.Q [in Continuity.BI]
GeneralisedBarInduction.R [in Continuity.BI]
I
Intensional_Dialogue.funext [in Continuity.continuity_zoo_Prop]Intensional_Dialogue.R [in Continuity.continuity_zoo_Prop]
Intensional_Dialogue.A [in Continuity.continuity_zoo_Prop]
Intensional_Dialogue.Q [in Continuity.continuity_zoo_Prop]
K
Kawai.A [in Continuity.kawai2018]Kawai.R [in Continuity.kawai2018]
M
MinEx.B [in Continuity.BredeHerbelin.minimal_example]Modulus.A [in Continuity.continuity_zoo_Prop]
Modulus.Q [in Continuity.continuity_zoo_Prop]
Modulus.R [in Continuity.continuity_zoo_Prop]
N
nat_queries.R [in Continuity.continuity_zoo_Prop]nat_queries.A [in Continuity.continuity_zoo_Prop]
O
Ord.A [in Continuity.BredeHerbelin.brede_herbelin]S
sec.A [in Continuity.continuity_zoo_Prop]sec.R [in Continuity.continuity_zoo_Prop]
T
TreeFunction.A [in Continuity.continuity_zoo_Prop]TreeFunction.Q [in Continuity.continuity_zoo_Prop]
TreeFunction.R [in Continuity.continuity_zoo_Prop]
Library Index
B
BIbrede_herbelin
Brouwer_ext
C
cantorClassical
continuity_zoo_Prop
E
extra_principlesK
kawai2018M
minimal_exampleU
UtilLemma Index
A
ABapprox_PtoT_pruning [in Continuity.BredeHerbelin.brede_herbelin]ABapprox_pruning_TtoP [in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_choicefun [in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_barred_TtoP_size_inf [in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_PtoT_barred [in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_barred_TtoP [in Continuity.BredeHerbelin.brede_herbelin]
ABchoice_PtoT_choice [in Continuity.BredeHerbelin.brede_herbelin]
ABchoice_choice_TtoP [in Continuity.BredeHerbelin.brede_herbelin]
ABDownmonot_monotone [in Continuity.BredeHerbelin.brede_herbelin]
ABDown_PtoT_P [in Continuity.BredeHerbelin.brede_herbelin]
ABmonot_barred [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonot_monotone [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmono_size_dec [in Continuity.BredeHerbelin.brede_herbelin]
ABUpsize_monotone_size [in Continuity.BredeHerbelin.brede_herbelin]
ABUp_Up_dec [in Continuity.BredeHerbelin.brede_herbelin]
Add_induction_step [in Continuity.BI]
Add_cat [in Continuity.BI]
Add_rcons [in Continuity.BI]
all_uniform [in Continuity.continuity_zoo_Prop]
arbor_is_tree [in Continuity.BredeHerbelin.brede_herbelin]
B
barred_ABbarred_PtoT_Up [in Continuity.BredeHerbelin.brede_herbelin]barred_barred_Upmon [in Continuity.BredeHerbelin.brede_herbelin]
barred_ABbarred_PtoT [in Continuity.BredeHerbelin.brede_herbelin]
barred_TtoP_ABbarred [in Continuity.BredeHerbelin.brede_herbelin]
barred_Bseq_cont [in Continuity.BI]
barred_Bseq_cont_aux [in Continuity.BI]
BbetaP [in Continuity.continuity_zoo_Prop]
Bcoind_dial_cont_to_neigh_cont [in Continuity.kawai2018]
Beval_ext_tree_monotone [in Continuity.Brouwer_ext]
Beval_ext_tree_output_unique [in Continuity.Brouwer_ext]
Beval_ext_tree_constant [in Continuity.Brouwer_ext]
Beval_ext_tree_map_aux [in Continuity.Brouwer_ext]
beval_list_modulus_at [in Continuity.BI]
beval_list_barred [in Continuity.BI]
beval_list_barred_aux [in Continuity.BI]
beval_list_mon [in Continuity.BI]
beval_ext [in Continuity.BI]
Bieval_output_unique [in Continuity.Brouwer_ext]
Bieval_monotone_plus [in Continuity.Brouwer_ext]
Bieval_monotone [in Continuity.Brouwer_ext]
Bieval_trace_inf [in Continuity.kawai2018]
Bieval_trace_Some [in Continuity.kawai2018]
Bieval_pred_trace [in Continuity.BI]
Bieval_trace_spec [in Continuity.BI]
Bieval_pred_to_Bitree_spec [in Continuity.BI]
Bitree_cont_to_itree_cont [in Continuity.Brouwer_ext]
Bitree_to_itreeP [in Continuity.Brouwer_ext]
Bitree_to_itreeP_aux [in Continuity.Brouwer_ext]
Bitree_to_option_Bieval [in Continuity.Brouwer_ext]
BI_GBI_alt [in Continuity.BredeHerbelin.brede_herbelin]
BI_GBI_dec [in Continuity.BredeHerbelin.brede_herbelin]
BI_GBI [in Continuity.BredeHerbelin.brede_herbelin]
Bneigh_cont_equiv_dialogue_cont_Brouwer [in Continuity.kawai2018]
Bneigh_continuous_neigh_continuous [in Continuity.kawai2018]
Brouwer_operation_at_Type_spec [in Continuity.kawai2018]
Brouwer_operation_at'_spec1 [in Continuity.kawai2018]
Brouwer_operation_at_spec [in Continuity.kawai2018]
Bseq_cont_to_dialogue_cont_Brouwer [in Continuity.BI]
Btree_to_dialogueP [in Continuity.continuity_zoo_Prop]
Btree_to_dialogueP_aux [in Continuity.continuity_zoo_Prop]
Bvalid_every_list [in Continuity.Brouwer_ext]
Bvalid_plus [in Continuity.Brouwer_ext]
C
cantor [in Continuity.BredeHerbelin.cantor]Cantor_Prop [in Continuity.BredeHerbelin.cantor]
case_to_false [in Continuity.BredeHerbelin.cantor]
choicefun_Downarbor_choicefun [in Continuity.BredeHerbelin.brede_herbelin]
choice_ABchoice_PtoT [in Continuity.BredeHerbelin.brede_herbelin]
choice_TtoP_ABchoice [in Continuity.BredeHerbelin.brede_herbelin]
CI_imp_c_BI [in Continuity.BI]
CoCI_BI [in Continuity.BI]
coind_dial_cont_to_tree_fun_cont [in Continuity.continuity_zoo_Prop]
continuous_via_interrogations_iff [in Continuity.continuity_zoo_Prop]
c_BI_imp_CI [in Continuity.BI]
D
decidable_iff [in Continuity.Util]Delta0_choice [in Continuity.continuity_zoo_Prop]
dialogue_is_uniform [in Continuity.continuity_zoo_Prop]
dialogue_not_uniform [in Continuity.continuity_zoo_Prop]
dialogue_F [in Continuity.continuity_zoo_Prop]
dialogue_to_tree_fun_cont [in Continuity.continuity_zoo_Prop]
dialogue_to_ext_tree_for [in Continuity.continuity_zoo_Prop]
dialogue_to_ext_tree_wf [in Continuity.continuity_zoo_Prop]
dialogue_to_btree_cont [in Continuity.continuity_zoo_Prop]
dialogue_to_BtreeP [in Continuity.continuity_zoo_Prop]
dialogue_cont_Brouwer_to_dialogue_cont [in Continuity.continuity_zoo_Prop]
dialogue_cont_to_is_dialogue [in Continuity.continuity_zoo_Prop]
dialogue_is_dialogue [in Continuity.continuity_zoo_Prop]
DNS [in Continuity.Classical]
DownABarbor_is_tree [in Continuity.BredeHerbelin.brede_herbelin]
E
eq_catr [in Continuity.continuity_zoo_Prop]eq_catl [in Continuity.continuity_zoo_Prop]
eq_cat [in Continuity.continuity_zoo_Prop]
eval_ext_tree_pref_monotone [in Continuity.Brouwer_ext]
eval_ext_tree_pref_monotone_aux [in Continuity.Brouwer_ext]
eval_ext_tree_trace_from_pref [in Continuity.Brouwer_ext]
eval_ext_tree_from_pref [in Continuity.Brouwer_ext]
eval_list_map_In [in Continuity.BI]
eval_list_incl_none [in Continuity.BI]
eval_list_monotone [in Continuity.BI]
eval_list_notin_cat [in Continuity.BI]
eval_list_none_fun [in Continuity.BI]
eval_list_notin [in Continuity.BI]
eval_list_In_is_fun [in Continuity.BI]
eval_list_In [in Continuity.BI]
eval_modulus_to_ext [in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_continuous [in Continuity.continuity_zoo_Prop]
eval_ext_tree_continuous [in Continuity.continuity_zoo_Prop]
eval_ext_tree_valid_eqtau [in Continuity.continuity_zoo_Prop]
eval_ext_tree_to_interrogation [in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_size_eval_trace [in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_size_eval [in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_monotone [in Continuity.continuity_zoo_Prop]
eval_ext_tree_monotone [in Continuity.continuity_zoo_Prop]
eval_ext_tree_map [in Continuity.continuity_zoo_Prop]
eval_ext_tree_map_aux [in Continuity.continuity_zoo_Prop]
eval_ext_tree_output_unique [in Continuity.continuity_zoo_Prop]
eval_ext_tree_constant [in Continuity.continuity_zoo_Prop]
eval_ext_tree_ext [in Continuity.continuity_zoo_Prop]
extree_to_Bextree_noo_eq [in Continuity.Brouwer_ext]
extree_to_Bextree_spec [in Continuity.Brouwer_ext]
ext_tree_to_Bext_tree_valid [in Continuity.Brouwer_ext]
ext_tree_valid_eqtau_ask [in Continuity.continuity_zoo_Prop]
ext_tree_valid_valid [in Continuity.continuity_zoo_Prop]
ex_modulus_modulus_fun [in Continuity.continuity_zoo_Prop]
F
fixed_magic_size [in Continuity.BredeHerbelin.brede_herbelin]fixed_magic_incl [in Continuity.BredeHerbelin.brede_herbelin]
followP [in Continuity.continuity_zoo_Prop]
from_pref_finite_equal [in Continuity.Brouwer_ext]
from_pref_map_iota [in Continuity.Brouwer_ext]
G
GBI_BI_alt [in Continuity.BredeHerbelin.brede_herbelin]GBI_inconsistent [in Continuity.BredeHerbelin.brede_herbelin]
GBI_monot_dec [in Continuity.BredeHerbelin.brede_herbelin]
GBI_BI_dec [in Continuity.BredeHerbelin.brede_herbelin]
GBI_monot [in Continuity.BredeHerbelin.brede_herbelin]
GBI_GCI [in Continuity.BI]
GBI_GCI_Fail [in Continuity.BI]
GDC_inconsistent [in Continuity.BredeHerbelin.brede_herbelin]
GDC_tree [in Continuity.BredeHerbelin.brede_herbelin]
H
hereditary_closure_rect [in Continuity.extra_principles]hereditary_closure_Acc [in Continuity.extra_principles]
hered_Upmon_hered_dec [in Continuity.BredeHerbelin.brede_herbelin]
hered_Upmon_hered [in Continuity.BredeHerbelin.brede_herbelin]
I
ieval_finapp_one_step_fuel [in Continuity.BI]ieval_finapp_trace [in Continuity.BI]
ieval_finapp_monotone_ask_list_nomorefuel [in Continuity.BI]
ieval_finapp_monotone_ask_fuel [in Continuity.BI]
ieval_finapp_monotone_ask_list [in Continuity.BI]
ieval_finapp_monotone_output_fuel [in Continuity.BI]
ieval_finapp_monotone_output_list [in Continuity.BI]
ieval_output_unique [in Continuity.continuity_zoo_Prop]
inclP [in Continuity.Util]
included_size [in Continuity.BredeHerbelin.brede_herbelin]
incl_iota_max [in Continuity.BredeHerbelin.brede_herbelin]
inconsistent [in Continuity.Classical]
indbarred_inductively_barred_dual [in Continuity.BredeHerbelin.brede_herbelin]
indbarred_inductively_barred_Down_dual [in Continuity.BredeHerbelin.brede_herbelin]
indbarred_inductively_barred [in Continuity.BredeHerbelin.brede_herbelin]
indbarred_fun_list_itree_indbarredP [in Continuity.BI]
indbarred_fun_list_itree_indbarredP_aux [in Continuity.BI]
inductively_barred_indbarred_dual [in Continuity.BredeHerbelin.brede_herbelin]
inductively_barred_indbarred_Down_dual [in Continuity.BredeHerbelin.brede_herbelin]
inductively_barred_indbarred [in Continuity.BredeHerbelin.brede_herbelin]
InP [in Continuity.Util]
interrogation_equiv_eval_ext_tree [in Continuity.continuity_zoo_Prop]
interrogation_app [in Continuity.continuity_zoo_Prop]
interrogation_ext [in Continuity.continuity_zoo_Prop]
interrogation_cons [in Continuity.continuity_zoo_Prop]
interrogation_plus [in Continuity.continuity_zoo_Prop]
int_tree_to_ext_tree_one_step [in Continuity.continuity_zoo_Prop]
int_dialogue_cont_to_dialogue_cont [in Continuity.continuity_zoo_Prop]
inversion_ask [in Continuity.continuity_zoo_Prop]
in_iota [in Continuity.BredeHerbelin.brede_herbelin]
in_map [in Continuity.BredeHerbelin.brede_herbelin]
In_eval_list [in Continuity.BI]
iota_rcons [in Continuity.Util]
is_fun_rcons_notin_dom [in Continuity.BI]
is_fun_cons_notin_dom [in Continuity.BI]
is_fun_cat_notin_dom [in Continuity.BI]
is_fun_list_incl [in Continuity.BI]
is_fun_map [in Continuity.BI]
is_dialogue_to_dialogue [in Continuity.continuity_zoo_Prop]
is_dialogue_to_dialogue_ext [in Continuity.continuity_zoo_Prop]
itree_to_Bitree_cont [in Continuity.Brouwer_ext]
itree_to_BitreeP [in Continuity.Brouwer_ext]
itree_to_Bitree_seq [in Continuity.Brouwer_ext]
itree_indbarredP_change_fuel [in Continuity.BI]
itree_indbarredP_monotone [in Continuity.BI]
itree_indbarred_spec [in Continuity.BI]
itree_indbarredP_ind [in Continuity.BI]
itree_indbarred_dialogue [in Continuity.BI]
itree_indbarred_dialogue_aux [in Continuity.BI]
K
K0K [in Continuity.kawai2018]K0K_aux [in Continuity.kawai2018]
L
list_to_dialogue_eq [in Continuity.continuity_zoo_Prop]list_to_dialogue_deval_eq [in Continuity.continuity_zoo_Prop]
list_to_cantor_swap [in Continuity.continuity_zoo_Prop]
M
map_incl [in Continuity.BredeHerbelin.brede_herbelin]mem_fixed_magic [in Continuity.BredeHerbelin.brede_herbelin]
modulus_at_nat_to_modulus_at [in Continuity.continuity_zoo_Prop]
modulus_at_to_modulus_at_nat [in Continuity.continuity_zoo_Prop]
modulus_ex_modulus [in Continuity.continuity_zoo_Prop]
monotone_ABUp_PtoT_P [in Continuity.BredeHerbelin.brede_herbelin]
monot_barred [in Continuity.BredeHerbelin.brede_herbelin]
MP [in Continuity.Classical]
N
neighborhood_wf_valid_Bext_tree [in Continuity.kawai2018]neigh_cont_iff_Bcoind_dial_cont [in Continuity.kawai2018]
neigh_cont_to_Bcoind_dial_cont [in Continuity.kawai2018]
neigh_cont_Btree_fun_cont [in Continuity.kawai2018]
neigh_realises_Beval [in Continuity.kawai2018]
neigh_realises_Beval_aux [in Continuity.kawai2018]
NoDupP [in Continuity.Util]
Notallin [in Continuity.Util]
nth_nth' [in Continuity.BI]
n_comp_n_plus [in Continuity.continuity_zoo_Prop]
O
ordP [in Continuity.BredeHerbelin.brede_herbelin]ord_dec [in Continuity.BredeHerbelin.brede_herbelin]
ord_iota_aux [in Continuity.BredeHerbelin.brede_herbelin]
ord_map_aux [in Continuity.BredeHerbelin.brede_herbelin]
ord_inf_size [in Continuity.BredeHerbelin.brede_herbelin]
ord_inf_size_aux [in Continuity.BredeHerbelin.brede_herbelin]
ord_incl' [in Continuity.BredeHerbelin.brede_herbelin]
ord_NoDup [in Continuity.BredeHerbelin.brede_herbelin]
ord_in_2 [in Continuity.BredeHerbelin.brede_herbelin]
ord_sizeu_notin [in Continuity.BredeHerbelin.brede_herbelin]
ord_notin [in Continuity.BredeHerbelin.brede_herbelin]
ord_incl [in Continuity.BredeHerbelin.brede_herbelin]
ord_nth_in [in Continuity.BredeHerbelin.brede_herbelin]
ord_in [in Continuity.BredeHerbelin.brede_herbelin]
ord_nth [in Continuity.BredeHerbelin.brede_herbelin]
ord_rcons [in Continuity.BredeHerbelin.brede_herbelin]
ord_size [in Continuity.BredeHerbelin.brede_herbelin]
ord_drop [in Continuity.BredeHerbelin.brede_herbelin]
ord_take [in Continuity.BredeHerbelin.brede_herbelin]
ord_cat [in Continuity.BredeHerbelin.brede_herbelin]
ord_inj [in Continuity.BredeHerbelin.brede_herbelin]
ord_map_snd [in Continuity.BredeHerbelin.brede_herbelin]
P
pref_a_Bieval [in Continuity.BI]pref_a_beval [in Continuity.BI]
pref_a_alpha [in Continuity.BI]
pref_a_eq [in Continuity.BI]
pref_padded_prefix [in Continuity.continuity_zoo_Prop]
pref_le_eq [in Continuity.continuity_zoo_Prop]
pruning_pruning_Downarbor [in Continuity.BredeHerbelin.brede_herbelin]
pruning_ABapprox_PtoT [in Continuity.BredeHerbelin.brede_herbelin]
pruning_TtoP_ABapprox [in Continuity.BredeHerbelin.brede_herbelin]
pruning_cat [in Continuity.BredeHerbelin.brede_herbelin]
pruning_arbor [in Continuity.BredeHerbelin.minimal_example]
PtoT_dec [in Continuity.BredeHerbelin.brede_herbelin]
PtoT_TtoP_ret [in Continuity.BredeHerbelin.brede_herbelin]
PtoT_TtoP_inv [in Continuity.BredeHerbelin.brede_herbelin]
P_ABUp_PtoTB [in Continuity.BredeHerbelin.brede_herbelin]
P_ABDown_PtoT [in Continuity.BredeHerbelin.brede_herbelin]
P_Uparbor_PtoT [in Continuity.BredeHerbelin.brede_herbelin]
R
reify [in Continuity.continuity_zoo_Prop]reify2 [in Continuity.continuity_zoo_Prop]
retraction_Lawvere [in Continuity.BredeHerbelin.cantor]
S
self_modulus_tree_fun_cont [in Continuity.continuity_zoo_Prop]size_ord [in Continuity.BredeHerbelin.brede_herbelin]
T
test [in Continuity.BredeHerbelin.minimal_example]Theorem5 [in Continuity.BredeHerbelin.brede_herbelin]
Theorem5rev [in Continuity.BredeHerbelin.brede_herbelin]
top_cons [in Continuity.BredeHerbelin.brede_herbelin]
tree_fun_cont_to_Brouwer [in Continuity.Brouwer_ext]
tree_fun_cont_to_Brouwer_aux [in Continuity.Brouwer_ext]
tree_fun_cont_equiv_self_modulus_cont [in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_self_modulus_cont [in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_tree_fun_cont_valid [in Continuity.continuity_zoo_Prop]
tree_fun_cont_iff_coind_dial_cont [in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_coind_dial_cont [in Continuity.continuity_zoo_Prop]
tree_fun_cont_wf_to_tree_fun_cont [in Continuity.continuity_zoo_Prop]
TtoP_PtoT_inv [in Continuity.BredeHerbelin.brede_herbelin]
T14 [in Continuity.continuity_zoo_Prop]
T41 [in Continuity.continuity_zoo_Prop]
U
uniform_is_dialogue [in Continuity.continuity_zoo_Prop]unzip1_ord [in Continuity.BredeHerbelin.brede_herbelin]
unzip2_ord [in Continuity.BredeHerbelin.brede_herbelin]
UpABarbor_is_tree [in Continuity.BredeHerbelin.brede_herbelin]
Uparbor_PtoT_P [in Continuity.BredeHerbelin.brede_herbelin]
UpmonotonisationP [in Continuity.BredeHerbelin.brede_herbelin]
Upmonot_monotone [in Continuity.BredeHerbelin.brede_herbelin]
Upmono_dec [in Continuity.BredeHerbelin.brede_herbelin]
upP [in Continuity.BredeHerbelin.brede_herbelin]
useless_hypothesis [in Continuity.kawai2018]
V
valid_cat [in Continuity.continuity_zoo_Prop]Constructor Index
A
approx [in Continuity.BredeHerbelin.brede_herbelin]Ask [in Continuity.continuity_zoo_Prop]
ask [in Continuity.continuity_zoo_Prop]
B
Bbeta_dep [in Continuity.continuity_zoo_Prop]Bconst [in Continuity.kawai2018]
Bconst_at [in Continuity.kawai2018]
Beta [in Continuity.BredeHerbelin.brede_herbelin]
beta [in Continuity.continuity_zoo_Prop]
Beta_dep [in Continuity.continuity_zoo_Prop]
bite [in Continuity.continuity_zoo_Prop]
Bret [in Continuity.Brouwer_ext]
Bsup [in Continuity.kawai2018]
Bsup_at_Type [in Continuity.kawai2018]
Bsup_at' [in Continuity.kawai2018]
Bsup_at [in Continuity.kawai2018]
Bvis [in Continuity.Brouwer_ext]
E
Eta [in Continuity.BredeHerbelin.brede_herbelin]eta [in Continuity.continuity_zoo_Prop]
H
hereditary_sons [in Continuity.extra_principles]hereditary_self [in Continuity.extra_principles]
hereditary_sons [in Continuity.BredeHerbelin.minimal_example]
hereditary_self [in Continuity.BredeHerbelin.minimal_example]
I
ibeta [in Continuity.BredeHerbelin.brede_herbelin]ieta [in Continuity.BredeHerbelin.brede_herbelin]
inverse [in Continuity.BredeHerbelin.cantor]
itree_in [in Continuity.BI]
itree_beta [in Continuity.BI]
itree_succ [in Continuity.BI]
itree_eta [in Continuity.BI]
M
mon [in Continuity.BredeHerbelin.brede_herbelin]mon [in Continuity.BredeHerbelin.minimal_example]
N
NoQuestions [in Continuity.continuity_zoo_Prop]normask [in Continuity.continuity_zoo_Prop]
normret [in Continuity.continuity_zoo_Prop]
normsucccons [in Continuity.continuity_zoo_Prop]
normsuccnil [in Continuity.continuity_zoo_Prop]
normzerocons [in Continuity.continuity_zoo_Prop]
normzeronil [in Continuity.continuity_zoo_Prop]
O
output [in Continuity.continuity_zoo_Prop]P
prune [in Continuity.BredeHerbelin.brede_herbelin]prune [in Continuity.BredeHerbelin.minimal_example]
ptot [in Continuity.BredeHerbelin.brede_herbelin]
R
ret [in Continuity.continuity_zoo_Prop]Ret [in Continuity.continuity_zoo_Prop]
S
sefl_mon [in Continuity.BredeHerbelin.brede_herbelin]sons_mon [in Continuity.BredeHerbelin.brede_herbelin]
spit [in Continuity.continuity_zoo_Prop]
T
Tarbor [in Continuity.BredeHerbelin.brede_herbelin]Tau [in Continuity.continuity_zoo_Prop]
tbeta [in Continuity.continuity_zoo_Prop]
teta [in Continuity.continuity_zoo_Prop]
Tmon [in Continuity.BredeHerbelin.brede_herbelin]
Tmon_size [in Continuity.BredeHerbelin.brede_herbelin]
V
vis [in Continuity.continuity_zoo_Prop]Vis [in Continuity.continuity_zoo_Prop]
Inductive Index
A
ABapprox [in Continuity.BredeHerbelin.brede_herbelin]ABUparborification [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_size [in Continuity.BredeHerbelin.brede_herbelin]
B
Bitree [in Continuity.Brouwer_ext]Brouwer_operation_at_Type [in Continuity.kawai2018]
Brouwer_operation_at' [in Continuity.kawai2018]
Brouwer_operation_at [in Continuity.kawai2018]
Brouwer_operation [in Continuity.kawai2018]
Btree [in Continuity.continuity_zoo_Prop]
Btree_dep [in Continuity.continuity_zoo_Prop]
D
dialogue [in Continuity.continuity_zoo_Prop]H
hereditary_closure [in Continuity.extra_principles]hereditary_closure [in Continuity.BredeHerbelin.minimal_example]
hered_mon [in Continuity.BredeHerbelin.brede_herbelin]
I
indbarred [in Continuity.BredeHerbelin.brede_herbelin]indbarred_spec [in Continuity.BredeHerbelin.brede_herbelin]
interrogation [in Continuity.continuity_zoo_Prop]
is_dialogue [in Continuity.continuity_zoo_Prop]
Itree [in Continuity.continuity_zoo_Prop]
itree [in Continuity.continuity_zoo_Prop]
itree_indbarredP [in Continuity.BI]
itree_indbarred [in Continuity.BI]
N
norm1 [in Continuity.continuity_zoo_Prop]norm2 [in Continuity.continuity_zoo_Prop]
P
pruning [in Continuity.BredeHerbelin.brede_herbelin]pruning [in Continuity.BredeHerbelin.minimal_example]
PtoT [in Continuity.BredeHerbelin.brede_herbelin]
R
result [in Continuity.continuity_zoo_Prop]right_invertible [in Continuity.BredeHerbelin.cantor]
U
Upmonotonisation [in Continuity.BredeHerbelin.brede_herbelin]Upmonotonisation [in Continuity.BredeHerbelin.minimal_example]
Section Index
A
Additional_Lemmas [in Continuity.BredeHerbelin.brede_herbelin]B
BarInduction [in Continuity.BI]Bars [in Continuity.extra_principles]
BI_mon [in Continuity.BredeHerbelin.brede_herbelin]
Brouwer [in Continuity.continuity_zoo_Prop]
Brouwer_interaction_trees [in Continuity.Brouwer_ext]
Brouwer_ext_tree [in Continuity.Brouwer_ext]
C
Cantor [in Continuity.continuity_zoo_Prop]Cantor.fix_types [in Continuity.continuity_zoo_Prop]
cBI_implies_CI_fail [in Continuity.BI]
continuity_principles [in Continuity.continuity_zoo_Prop]
ContinuousBarInduction [in Continuity.BI]
ContinuousInduction [in Continuity.BI]
D
DC_GDC_BI_GBI [in Continuity.BredeHerbelin.brede_herbelin]Dialogue_not_uniform [in Continuity.continuity_zoo_Prop]
F
FinQuestion [in Continuity.continuity_zoo_Prop]G
GBI_dec.Magic [in Continuity.BredeHerbelin.brede_herbelin]GBI_dec [in Continuity.BredeHerbelin.brede_herbelin]
GDC_gen [in Continuity.BredeHerbelin.brede_herbelin]
GDC_GBI_Definition [in Continuity.BredeHerbelin.brede_herbelin]
GeneralisedBarInduction [in Continuity.BI]
I
Intensional_Dialogue [in Continuity.continuity_zoo_Prop]K
Kawai [in Continuity.kawai2018]M
MinEx [in Continuity.BredeHerbelin.minimal_example]Modulus [in Continuity.continuity_zoo_Prop]
N
nat_queries [in Continuity.continuity_zoo_Prop]O
Ord [in Continuity.BredeHerbelin.brede_herbelin]S
sec [in Continuity.continuity_zoo_Prop]T
Technical [in Continuity.BredeHerbelin.brede_herbelin]TreeFunction [in Continuity.continuity_zoo_Prop]
Abbreviation Index
B
Brouwer [in Continuity.continuity_zoo_Prop]D
dialogue [in Continuity.continuity_zoo_Prop]I
itree [in Continuity.Brouwer_ext]Itree [in Continuity.BI]
Q
Q [in Continuity.Brouwer_ext]Q [in Continuity.Brouwer_ext]
Q [in Continuity.BI]
Q [in Continuity.BI]
Q [in Continuity.continuity_zoo_Prop]
Q [in Continuity.continuity_zoo_Prop]
Q [in Continuity.continuity_zoo_Prop]
R
R [in Continuity.BI]Definition Index
A
ABbarred [in Continuity.BredeHerbelin.brede_herbelin]ABchoicefun [in Continuity.BredeHerbelin.brede_herbelin]
ABDownarborification [in Continuity.BredeHerbelin.brede_herbelin]
ABDownmonotonisation [in Continuity.BredeHerbelin.brede_herbelin]
ABis_tree [in Continuity.BredeHerbelin.brede_herbelin]
ABmonotone [in Continuity.BredeHerbelin.brede_herbelin]
ABmonotone_size [in Continuity.BredeHerbelin.brede_herbelin]
ABUparborification_sind [in Continuity.BredeHerbelin.brede_herbelin]
ABUparborification_ind [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_size_sind [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_size_ind [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_sind [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_ind [in Continuity.BredeHerbelin.brede_herbelin]
B
barred [in Continuity.extra_principles]Bbeta [in Continuity.continuity_zoo_Prop]
Bcoind_dial_cont [in Continuity.Brouwer_ext]
beval [in Continuity.continuity_zoo_Prop]
Beval_ext_tree_trace [in Continuity.Brouwer_ext]
Beval_ext_tree_trace_aux [in Continuity.Brouwer_ext]
Beval_ext_tree [in Continuity.Brouwer_ext]
Beval_ext_tree_aux [in Continuity.Brouwer_ext]
beval_list [in Continuity.BI]
beval_trace [in Continuity.BI]
Bext_tree [in Continuity.Brouwer_ext]
Bieval [in Continuity.Brouwer_ext]
Bieval_trace [in Continuity.kawai2018]
Bieval_trace [in Continuity.BI]
BIProp11Down [in Continuity.BredeHerbelin.brede_herbelin]
BIProp11Down_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp11Up [in Continuity.BredeHerbelin.brede_herbelin]
BIProp11Up_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp12 [in Continuity.BredeHerbelin.brede_herbelin]
BIProp12Up [in Continuity.BredeHerbelin.brede_herbelin]
BIProp12Up_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp12_sym_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp12_sym [in Continuity.BredeHerbelin.brede_herbelin]
BIProp12_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp13 [in Continuity.BredeHerbelin.brede_herbelin]
BIProp13Down [in Continuity.BredeHerbelin.brede_herbelin]
BIProp13Down_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp13Up_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp13_rev [in Continuity.BredeHerbelin.brede_herbelin]
Bitree_to_itree [in Continuity.Brouwer_ext]
Bitree_to_itree_aux [in Continuity.Brouwer_ext]
Bitree_to_option [in Continuity.Brouwer_ext]
BI_alt [in Continuity.BredeHerbelin.brede_herbelin]
BI_ind [in Continuity.extra_principles]
Bneigh_cont [in Continuity.kawai2018]
Brouwer_operation_at_Type_sind [in Continuity.kawai2018]
Brouwer_operation_at_Type_rec [in Continuity.kawai2018]
Brouwer_operation_at_Type_ind [in Continuity.kawai2018]
Brouwer_operation_at_Type_rect [in Continuity.kawai2018]
Brouwer_operation_at'_sind [in Continuity.kawai2018]
Brouwer_operation_at'_rec [in Continuity.kawai2018]
Brouwer_operation_at'_ind [in Continuity.kawai2018]
Brouwer_operation_at'_rect [in Continuity.kawai2018]
Brouwer_operation_at_sind [in Continuity.kawai2018]
Brouwer_operation_at_ind [in Continuity.kawai2018]
Brouwer_operation_sind [in Continuity.kawai2018]
Brouwer_operation_ind [in Continuity.kawai2018]
Btree_fun_cont_valid [in Continuity.Brouwer_ext]
Btree_fun_cont [in Continuity.Brouwer_ext]
Btree_to_dialogue [in Continuity.continuity_zoo_Prop]
Btree_to_dialogue_aux [in Continuity.continuity_zoo_Prop]
Btree_dep_sind [in Continuity.continuity_zoo_Prop]
Btree_dep_rec [in Continuity.continuity_zoo_Prop]
Btree_dep_ind [in Continuity.continuity_zoo_Prop]
Btree_dep_rect [in Continuity.continuity_zoo_Prop]
Btree_sind [in Continuity.continuity_zoo_Prop]
Btree_rec [in Continuity.continuity_zoo_Prop]
Btree_ind [in Continuity.continuity_zoo_Prop]
Btree_rect [in Continuity.continuity_zoo_Prop]
Bvalid_ext_tree [in Continuity.Brouwer_ext]
C
choicefun [in Continuity.BredeHerbelin.brede_herbelin]coind_dial_cont [in Continuity.continuity_zoo_Prop]
comp_modulus_cont [in Continuity.continuity_zoo_Prop]
Cont [in Continuity.Classical]
continuous_modulus_cont_nat [in Continuity.continuity_zoo_Prop]
continuous_modulus_cont [in Continuity.continuity_zoo_Prop]
c_BI [in Continuity.BI]
c_bar [in Continuity.BI]
D
DC [in Continuity.BredeHerbelin.brede_herbelin]DCProp11 [in Continuity.BredeHerbelin.brede_herbelin]
DCProp11_rev [in Continuity.BredeHerbelin.brede_herbelin]
DCProp12 [in Continuity.BredeHerbelin.brede_herbelin]
DCProp12_sym_rev [in Continuity.BredeHerbelin.brede_herbelin]
DCProp12_sym [in Continuity.BredeHerbelin.brede_herbelin]
DCProp12_rev [in Continuity.BredeHerbelin.brede_herbelin]
DCProp13 [in Continuity.BredeHerbelin.brede_herbelin]
DCProp13_sym_rev [in Continuity.BredeHerbelin.brede_herbelin]
DCProp13_sym [in Continuity.BredeHerbelin.brede_herbelin]
DCProp13_rev [in Continuity.BredeHerbelin.brede_herbelin]
deval [in Continuity.continuity_zoo_Prop]
deval_list_to_dialogue_trace [in Continuity.continuity_zoo_Prop]
dialogue_to_list [in Continuity.continuity_zoo_Prop]
dialogue_to_ext_tree [in Continuity.continuity_zoo_Prop]
dialogue_to_Btree [in Continuity.continuity_zoo_Prop]
dialogue_to_Brouwer [in Continuity.continuity_zoo_Prop]
dialogue_cont_Brouwer [in Continuity.continuity_zoo_Prop]
dialogue_cont [in Continuity.continuity_zoo_Prop]
dialogue_sind [in Continuity.continuity_zoo_Prop]
dialogue_rec [in Continuity.continuity_zoo_Prop]
dialogue_ind [in Continuity.continuity_zoo_Prop]
dialogue_rect [in Continuity.continuity_zoo_Prop]
DNE [in Continuity.Classical]
Downarborification [in Continuity.BredeHerbelin.brede_herbelin]
Downarborification [in Continuity.BredeHerbelin.minimal_example]
Downmonotonisation [in Continuity.BredeHerbelin.brede_herbelin]
E
eval_list [in Continuity.BI]eval_ext_tree_trace [in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_aux [in Continuity.continuity_zoo_Prop]
eval_ext_tree [in Continuity.continuity_zoo_Prop]
eval_ext_tree_aux [in Continuity.continuity_zoo_Prop]
extree_to_Bextree_noo [in Continuity.Brouwer_ext]
extree_to_Bextree [in Continuity.Brouwer_ext]
extree_to_extree [in Continuity.Brouwer_ext]
ext_tree_valid [in Continuity.continuity_zoo_Prop]
ext_tree_valid_aux [in Continuity.continuity_zoo_Prop]
ext_tree_to_int_tree [in Continuity.continuity_zoo_Prop]
ext_tree_for [in Continuity.continuity_zoo_Prop]
ext_tree [in Continuity.continuity_zoo_Prop]
ex_modulus_cont_nat [in Continuity.continuity_zoo_Prop]
ex_modulus_cont [in Continuity.continuity_zoo_Prop]
F
F [in Continuity.continuity_zoo_Prop]fixed_magic [in Continuity.BredeHerbelin.brede_herbelin]
follow [in Continuity.continuity_zoo_Prop]
from_pref [in Continuity.continuity_zoo_Prop]
G
GBI [in Continuity.BredeHerbelin.brede_herbelin]GDC [in Continuity.BredeHerbelin.brede_herbelin]
H
hereditary_closure_sind [in Continuity.extra_principles]hereditary_closure_ind [in Continuity.extra_principles]
hereditary_closure_sind [in Continuity.BredeHerbelin.minimal_example]
hereditary_closure_rec [in Continuity.BredeHerbelin.minimal_example]
hereditary_closure_ind [in Continuity.BredeHerbelin.minimal_example]
hereditary_closure_rect [in Continuity.BredeHerbelin.minimal_example]
hered_mon_sind [in Continuity.BredeHerbelin.brede_herbelin]
hered_mon_ind [in Continuity.BredeHerbelin.brede_herbelin]
I
ieval [in Continuity.continuity_zoo_Prop]ieval_trace [in Continuity.BI]
ieval_finapp [in Continuity.BI]
indbarred_spec_sind [in Continuity.BredeHerbelin.brede_herbelin]
indbarred_spec_ind [in Continuity.BredeHerbelin.brede_herbelin]
indbarred_sind [in Continuity.BredeHerbelin.brede_herbelin]
indbarred_ind [in Continuity.BredeHerbelin.brede_herbelin]
inductively_barred [in Continuity.extra_principles]
interrogation_sind [in Continuity.continuity_zoo_Prop]
interrogation_ind [in Continuity.continuity_zoo_Prop]
int_tree_to_ext_tree [in Continuity.continuity_zoo_Prop]
int_dialogue_cont [in Continuity.continuity_zoo_Prop]
is_tree [in Continuity.BredeHerbelin.brede_herbelin]
is_fun_list [in Continuity.BI]
is_dialogue_sind [in Continuity.continuity_zoo_Prop]
is_dialogue_rec [in Continuity.continuity_zoo_Prop]
is_dialogue_ind [in Continuity.continuity_zoo_Prop]
is_dialogue_rect [in Continuity.continuity_zoo_Prop]
itree_to_Bitree [in Continuity.Brouwer_ext]
itree_indbarredP_rect [in Continuity.BI]
itree_indbarred_sind [in Continuity.BI]
itree_indbarred_rec [in Continuity.BI]
itree_indbarred_ind [in Continuity.BI]
itree_indbarred_rect [in Continuity.BI]
L
list_to_dialogue [in Continuity.continuity_zoo_Prop]list_to_cantor [in Continuity.continuity_zoo_Prop]
M
modulus [in Continuity.continuity_zoo_Prop]modulus_to_ext_tree [in Continuity.continuity_zoo_Prop]
modulus_nat [in Continuity.continuity_zoo_Prop]
modulus_at_nat [in Continuity.continuity_zoo_Prop]
modulus_at [in Continuity.continuity_zoo_Prop]
monotone [in Continuity.BredeHerbelin.brede_herbelin]
N
neighborhoodfunction [in Continuity.kawai2018]neigh_to_Bitree [in Continuity.kawai2018]
neigh_cont [in Continuity.kawai2018]
neigh_realises [in Continuity.kawai2018]
norm1_sind [in Continuity.continuity_zoo_Prop]
norm1_rec [in Continuity.continuity_zoo_Prop]
norm1_ind [in Continuity.continuity_zoo_Prop]
norm1_rect [in Continuity.continuity_zoo_Prop]
norm2_sind [in Continuity.continuity_zoo_Prop]
norm2_rec [in Continuity.continuity_zoo_Prop]
norm2_ind [in Continuity.continuity_zoo_Prop]
norm2_rect [in Continuity.continuity_zoo_Prop]
nth' [in Continuity.BI]
n_comp [in Continuity.continuity_zoo_Prop]
O
ord [in Continuity.BredeHerbelin.brede_herbelin]ord_aux [in Continuity.BredeHerbelin.brede_herbelin]
P
padded_prefix [in Continuity.continuity_zoo_Prop]padded_seq [in Continuity.continuity_zoo_Prop]
pred_to_fun [in Continuity.BI]
pred_to_Bitree_aux [in Continuity.BI]
pref [in Continuity.continuity_zoo_Prop]
prefix [in Continuity.extra_principles]
pref_a [in Continuity.BI]
PtoT_dual [in Continuity.BredeHerbelin.brede_herbelin]
PtoT_sind [in Continuity.BredeHerbelin.brede_herbelin]
PtoT_ind [in Continuity.BredeHerbelin.brede_herbelin]
R
reflect1 [in Continuity.continuity_zoo_Prop]reflect2 [in Continuity.continuity_zoo_Prop]
result_sind [in Continuity.continuity_zoo_Prop]
result_rec [in Continuity.continuity_zoo_Prop]
result_ind [in Continuity.continuity_zoo_Prop]
result_rect [in Continuity.continuity_zoo_Prop]
retract_of [in Continuity.Classical]
right_invertible_sind [in Continuity.BredeHerbelin.cantor]
right_invertible_ind [in Continuity.BredeHerbelin.cantor]
S
self_modulus_cont [in Continuity.continuity_zoo_Prop]T
top [in Continuity.BredeHerbelin.brede_herbelin]tree_fun_cont_valid [in Continuity.continuity_zoo_Prop]
tree_fun_cont_wf [in Continuity.continuity_zoo_Prop]
tree_fun_cont_via_interrogations [in Continuity.continuity_zoo_Prop]
tree_fun_cont [in Continuity.continuity_zoo_Prop]
TtoP [in Continuity.BredeHerbelin.brede_herbelin]
TtoP_PtoT_ret [in Continuity.BredeHerbelin.brede_herbelin]
U
uni_cont [in Continuity.continuity_zoo_Prop]Upmonotonisation_sind [in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation_ind [in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation_sind [in Continuity.BredeHerbelin.minimal_example]
Upmonotonisation_rec [in Continuity.BredeHerbelin.minimal_example]
Upmonotonisation_ind [in Continuity.BredeHerbelin.minimal_example]
Upmonotonisation_rect [in Continuity.BredeHerbelin.minimal_example]
V
valid_ext_tree [in Continuity.continuity_zoo_Prop]W
wf_Bext_tree [in Continuity.Brouwer_ext]wf_ext_tree [in Continuity.continuity_zoo_Prop]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (735 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (27 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (64 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (283 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (55 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (32 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (30 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (222 entries) |