# Theory CZH_Sets_IF

```(* Copyright 2021 (C) Mihails Milehins *)

section‹Operations on indexed families of sets›
theory CZH_Sets_IF
imports CZH_Sets_BRelations
begin

subsection‹Background›

text‹
This section presents results about the fundamental operations on the indexed
families of sets, such as unions and intersections of the indexed families
of sets, disjoint unions and infinite Cartesian products.

Certain elements of the content of this section were inspired by
elements of the content of \<^cite>‹"paulson_hereditarily_2013"›.
However, as previously, many other results were ported (with amendments) from
the main library of Isabelle/HOL.
›

abbreviation (input) imVLambda :: "V ⇒ (V ⇒ V) ⇒ V"
where "imVLambda A f ≡ (λa∈⇩∘A. f a) `⇩∘ A"

subsection‹Intersection of an indexed family of sets›

syntax "_VIFINTER" :: "pttrn ⇒ V ⇒ V ⇒ V"  (‹(3⋂⇩∘_∈⇩∘_./ _)› [0, 0, 10] 10)

translations "⋂⇩∘x∈⇩∘A. f" ⇌ "CONST VInter (CONST imVLambda A (λx. f))"

text‹Rules.›

lemma vifintersectionI[intro]:
assumes "I ≠ 0" and "⋀i. i ∈⇩∘ I ⟹ a ∈⇩∘ f i"
shows "a ∈⇩∘ (⋂⇩∘i∈⇩∘I. f i)"
using assms by (auto intro!: vsubset_antisym)

lemma vifintersectionD[dest]:
assumes "a ∈⇩∘ (⋂⇩∘i∈⇩∘I. f i)" and "i ∈⇩∘ I"
shows "a ∈⇩∘ f i"
using assms by blast

lemma vifintersectionE1[elim]:
assumes "a ∈⇩∘ (⋂⇩∘i∈⇩∘I. f i)" and "a ∈⇩∘ f i ⟹ P" and "i ∉⇩∘ I ⟹ P"
shows P
using assms by blast

lemma vifintersectionE3[elim]:
assumes "a ∈⇩∘ (⋂⇩∘i∈⇩∘I. f i)"
obtains "⋀i. i∈⇩∘I ⟹ a ∈⇩∘ f i"
using assms by blast

lemma vifintersectionE2[elim]:
assumes "a ∈⇩∘ (⋂⇩∘i∈⇩∘I. f i)"
obtains i where "i ∈⇩∘ I" and "a ∈⇩∘ f i"
using assms by (elim vifintersectionE3) (meson assms VInterE2 app_vimageE)

text‹Set operations.›

lemma vifintersection_vempty_is[simp]: "(⋂⇩∘i∈⇩∘0. f i) = 0" by auto

lemma vifintersection_vsingleton_is[simp]: "(⋂⇩∘i∈⇩∘set{i}. f i) = f i"
using elts_0 by blast

lemma vifintersection_vdoubleton_is[simp]: "(⋂⇩∘i∈⇩∘set {i, j}. f i) = f i ∩⇩∘ f j"
by
(
intro vsubset_antisym vsubsetI;
(elim vifintersectionE3 | intro vifintersectionI)
)
auto

lemma vifintersection_antimono1:
assumes "I ≠ 0" and "I ⊆⇩∘ J"
shows "(⋂⇩∘j∈⇩∘J. f j) ⊆⇩∘ (⋂⇩∘i∈⇩∘I. f i)"
using assms by blast

lemma vifintersection_antimono2:
assumes "I ≠ 0" and " I ⊆⇩∘ J" and "⋀i. i ∈⇩∘ I ⟹ f i ⊆⇩∘ g i"
shows "(⋂⇩∘j∈⇩∘J. f j) ⊆⇩∘ (⋂⇩∘i∈⇩∘I. g i)"
using assms by blast

lemma vifintersection_vintersection:
assumes "I ≠ 0" and "J ≠ 0"
shows "(⋂⇩∘i∈⇩∘I. f i) ∩⇩∘ (⋂⇩∘i∈⇩∘J. f i) = (⋂⇩∘i∈⇩∘I ∪⇩∘ J. f i)"
using assms by (auto intro!: vsubset_antisym)

lemma vifintersection_vintersection_family:
assumes "I ≠ 0"
shows "(⋂⇩∘i∈⇩∘I. A i) ∩⇩∘ (⋂⇩∘i∈⇩∘I. B i) = (⋂⇩∘i∈⇩∘I. A i ∩⇩∘ B i)"
using assms
by (intro vsubset_antisym vsubsetI, intro vifintersectionI | tactic‹all_tac›)
blast+

lemma vifintersection_vunion:
assumes "I ≠ 0" and "J ≠ 0"
shows "(⋂⇩∘i∈⇩∘I. f i) ∪⇩∘ (⋂⇩∘j∈⇩∘J. g j) = (⋂⇩∘i∈⇩∘I. ⋂⇩∘j∈⇩∘J. f i ∪⇩∘ g j)"
using assms by (blast intro!: vsubset_antisym)

lemma vifintersection_vinsert_is[intro, simp]:
assumes "I ≠ 0"
shows "(⋂⇩∘i ∈⇩∘ vinsert j I. f i) = f j ∩⇩∘ (⋂⇩∘i∈⇩∘I. f i)"
apply(insert assms, intro vsubset_antisym vsubsetI)
subgoal for b by (subgoal_tac ‹b ∈⇩∘ f j› ‹b ∈⇩∘ (⋂⇩∘i∈⇩∘I. f i)›) blast+
subgoal for b
by (subgoal_tac ‹b ∈⇩∘ f j› ‹b ∈⇩∘ (⋂⇩∘i∈⇩∘I. f i)›)
(blast intro!: vsubset_antisym)+
done

lemma vifintersection_VPow:
assumes "I ≠ 0"
shows "VPow (⋂⇩∘i∈⇩∘I. f i) = (⋂⇩∘i∈⇩∘I. VPow (f i))"
using assms by (auto intro!: vsubset_antisym)

text‹Elementary properties.›

lemma vifintersection_constant[intro, simp]:
assumes "I ≠ 0"
shows "(⋂⇩∘y∈⇩∘I. c) = c"
using assms by auto

lemma vifintersection_vsubset_iff:
assumes "I ≠ 0"
shows "A ⊆⇩∘ (⋂⇩∘i∈⇩∘I. f i) ⟷ (∀i∈⇩∘I. A ⊆⇩∘ f i)"
using assms by blast

lemma vifintersection_vsubset_lower:
assumes "i ∈⇩∘ I"
shows "(⋂⇩∘i∈⇩∘I. f i) ⊆⇩∘ f i"
using assms by blast

lemma vifintersection_vsubset_greatest:
assumes "I ≠ 0" and "⋀i. i ∈⇩∘ I ⟹ A ⊆⇩∘ f i"
shows "A ⊆⇩∘ (⋂⇩∘i∈⇩∘I. f i)"
using assms by (intro vsubsetI vifintersectionI) auto

lemma vifintersection_vintersection_value:
assumes "i ∈⇩∘ I"
shows "f i ∩⇩∘ (⋂⇩∘i∈⇩∘I. f i) = (⋂⇩∘i∈⇩∘I. f i)"
using assms by blast

lemma vifintersection_vintersection_single:
assumes "I ≠ 0"
shows "B ∪⇩∘ (⋂⇩∘i∈⇩∘I. A i) = (⋂⇩∘i∈⇩∘I. B ∪⇩∘ A i)"
by (insert assms, intro vsubset_antisym vsubsetI vifintersectionI)
blast+

text‹Connections.›

lemma vifintersection_vrange_VLambda: "(⋂⇩∘i∈⇩∘I. f i) = ⋂⇩∘ (ℛ⇩∘ (λa∈⇩∘I. f a))"
by (simp add: vimage_VLambda_vrange_rep)

subsection‹Union of an indexed family of sets›

syntax "_VIFUNION" :: "pttrn ⇒ V ⇒ V ⇒ V" (‹(3⋃⇩∘_∈⇩∘_./ _)› [0, 0, 10] 10)

translations "⋃⇩∘x∈⇩∘A. f" ⇌ "CONST VUnion (CONST imVLambda A (λx. f))"

text‹Rules.›

lemma vifunion_iff: "b ∈⇩∘ (⋃⇩∘i∈⇩∘I. f i) ⟷ (∃i∈⇩∘I. b ∈⇩∘ f i)" by force

lemma vifunionI[intro]:
assumes "i ∈⇩∘ I" and "a ∈⇩∘ f i"
shows "a ∈⇩∘ (⋃⇩∘i∈⇩∘I. f i)"
using assms by force

lemma vifunionD[dest]:
assumes "a ∈⇩∘ (⋃⇩∘i∈⇩∘I. f i)"
shows "∃i∈⇩∘I. a ∈⇩∘ f i"
using assms by auto

lemma vifunionE[elim!]:
assumes "a ∈⇩∘ (⋃⇩∘i∈⇩∘I. f i)" and "⋀i. ⟦ i ∈⇩∘ I; a ∈⇩∘ f i ⟧ ⟹ R"
shows R
using assms by auto

text‹Set operations.›

lemma vifunion_vempty_family[simp]: "(⋃⇩∘i∈⇩∘I. 0) = 0" by auto

lemma vifunion_vsingleton_is[simp]: "(⋃⇩∘i∈⇩∘set {i}. f i) = f i" by force

lemma vifunion_vsingleton_family[simp]: "(⋃⇩∘i∈⇩∘I. set {i}) = I" by force

lemma vifunion_vdoubleton: "(⋃⇩∘i∈⇩∘set {i, j}. f i) = f i ∪⇩∘ f j"
using VLambda_vinsert vimage_vunion_left
by (force simp: VLambda_vsingleton simp: vinsert_set_insert_eq)

lemma vifunion_mono:
assumes "I ⊆⇩∘ J" and "⋀i. i ∈⇩∘ I ⟹ f i ⊆⇩∘ g i"
shows "(⋃⇩∘i∈⇩∘I. f i) ⊆⇩∘ (⋃⇩∘j∈⇩∘J. g j)"
using assms by force

lemma vifunion_vunion_is: "(⋃⇩∘i∈⇩∘I. f i) ∪⇩∘ (⋃⇩∘j∈⇩∘J. f j) = (⋃⇩∘i∈⇩∘I ∪⇩∘ J. f i)"
by force

lemma vifunion_vunion_family:
"(⋃⇩∘i∈⇩∘I. f i) ∪⇩∘ (⋃⇩∘i∈⇩∘I. g i) = (⋃⇩∘i∈⇩∘I. f i ∪⇩∘ g i)"
by (intro vsubset_antisym vsubsetI; elim vunionE vifunionE) force+

lemma vifunion_vintersection:
"(⋃⇩∘i∈⇩∘I. f i) ∩⇩∘ (⋃⇩∘j∈⇩∘J. g j) = (⋃⇩∘i∈⇩∘I. ⋃⇩∘j∈⇩∘J. f i ∩⇩∘ g j)"
by (force simp: vrange_VLambda vimage_VLambda_vrange_rep)

lemma vifunion_vinsert_is:
"(⋃⇩∘i∈⇩∘vinsert j I. f i) = f j ∪⇩∘ (⋃⇩∘i∈⇩∘I. f i)"
by (force simp: vimage_VLambda_vrange_rep)

lemma vifunion_VPow: "(⋃⇩∘i∈⇩∘I. VPow (f i)) ⊆⇩∘ VPow (⋃⇩∘i∈⇩∘I. f i)" by force

text‹Elementary properties.›

lemma vifunion_vempty_conv:
"0 = (⋃⇩∘i∈⇩∘I. f i) ⟷ (∀i∈⇩∘I. f i = 0)"
"(⋃⇩∘i∈⇩∘I. f i) = 0 ⟷ (∀i∈⇩∘I. f i = 0)"
by (auto simp: vrange_VLambda vimage_VLambda_vrange_rep)

lemma vifunion_constant[simp]: "(⋃⇩∘i∈⇩∘I. c) = (if I = 0 then 0 else c)"
proof(intro vsubset_antisym)
show "(if I = 0 then 0 else c) ⊆⇩∘ (⋃⇩∘i∈⇩∘I. c)"
by (cases ‹vdisjnt I I›) (auto simp: VLambda_vconst_on)
qed auto

lemma vifunion_upper:
assumes "i ∈⇩∘ I"
shows "f i ⊆⇩∘ (⋃⇩∘i∈⇩∘I. f i)"
using assms by force

lemma vifunion_least:
assumes "⋀i. i ∈⇩∘ I ⟹ f i ⊆⇩∘ C"
shows "(⋃⇩∘i∈⇩∘I. f i) ⊆⇩∘ C"
using assms by auto

lemma vifunion_absorb:
assumes "j ∈⇩∘ I"
shows "f j ∪⇩∘ (⋃⇩∘i∈⇩∘I. f i) = (⋃⇩∘i∈⇩∘I. f i)"
using assms by force

lemma vifunion_vifunion_flatten:
"(⋃⇩∘j∈⇩∘(⋃⇩∘i∈⇩∘I. f i). g j) = (⋃⇩∘i∈⇩∘I. ⋃⇩∘j∈⇩∘f i. g j)"
by (force simp: vrange_VLambda vimage_VLambda_vrange_rep)

lemma vifunion_vsubset_iff: "((⋃⇩∘i∈⇩∘I. f i) ⊆⇩∘ B) = (∀i∈⇩∘I. f i ⊆⇩∘ B)" by force

lemma vifunion_vsingleton_eq_vrange: "(⋃⇩∘i∈⇩∘I. set {f i}) = ℛ⇩∘ (λa∈⇩∘I. f a)"
by force

lemma vball_vifunion[simp]: "(∀z∈⇩∘(⋃⇩∘i∈⇩∘I. f i). P z) ⟷ (∀x∈⇩∘I. ∀z∈⇩∘f x. P z)"
by force

lemma vbex_vifunion[simp]: "(∃z∈⇩∘(⋃⇩∘i∈⇩∘I. f i). P z) ⟷ (∃x∈⇩∘I. ∃z∈⇩∘f x. P z)"
by force

lemma vifunion_vintersection_index_right[simp]: "(⋃⇩∘C∈⇩∘B. A ∩⇩∘ C) = A ∩⇩∘ ⋃⇩∘B"
by (force simp: vimage_VLambda_vrange_rep)

lemma vifunion_vintersection_index_left[simp]: "(⋃⇩∘C∈⇩∘B. C ∩⇩∘ A) = ⋃⇩∘B ∩⇩∘ A"
by (force simp: vimage_VLambda_vrange_rep)

lemma vifunion_vunion_index[intro, simp]:
assumes "B ≠ 0"
shows "(⋂⇩∘C∈⇩∘B. A ∪⇩∘ C) = A ∪⇩∘ ⋂⇩∘B"
using assms
by
(
(intro vsubset_antisym vsubsetI);
(intro vifintersectionI | tactic‹all_tac›)
)
blast+

lemma vifunion_vintersection_single: "B ∩⇩∘ (⋃⇩∘i∈⇩∘I. f i) = (⋃⇩∘i∈⇩∘I. B ∩⇩∘ f i)"
by (force simp: vrange_VLambda vimage_VLambda_vrange_rep)

lemma vifunion_vifunion_flip:
"(⋃⇩∘b∈⇩∘B. ⋃⇩∘a∈⇩∘A. f b a) = (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. f b a)"
proof-
have "x ∈⇩∘ (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. f b a)" if "x ∈⇩∘ (⋃⇩∘b∈⇩∘B. ⋃⇩∘a∈⇩∘A. f b a)"
for x f A B
proof-
from that obtain b where b: "b ∈⇩∘ B" and x_b: "x ∈⇩∘ (⋃⇩∘a∈⇩∘A. f b a)"
by fastforce
then obtain a where a: "a ∈⇩∘ A" and x_fba: "x ∈⇩∘ f b a" by fastforce
show "x ∈⇩∘ (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. f b a)"
unfolding vifunion_iff by (auto intro: a b x_fba)
qed
then show ?thesis by (intro vsubset_antisym vsubsetI) auto
qed

text‹Connections.›

lemma vifunion_disjoint: "(⋃⇩∘C ∩⇩∘ A = 0) ⟷ (∀B∈⇩∘C. vdisjnt B A)"
by (intro iffI)
(auto intro!: vsubset_antisym simp: Sup_upper vdisjnt_vsubset_left)

lemma vdisjnt_vifunion_iff:
"vdisjnt A (⋃⇩∘i∈⇩∘I. f i) ⟷ (∀i∈⇩∘I. vdisjnt A (f i))"
by (force intro!: vsubset_antisym simp: vdisjnt_iff)+

lemma vifunion_VLambda: "(⋃⇩∘i∈⇩∘A. set {⟨i, f i⟩}) = (λa∈⇩∘A. f a)"
using vifunionI by (intro vsubset_antisym vsubsetI) auto

lemma vifunion_vrange_VLambda: "(⋃⇩∘i∈⇩∘I. f i) = ⋃⇩∘(ℛ⇩∘ (λa∈⇩∘I. f a))"
using vimage_VLambda_vrange_rep by auto

lemma (in vsv) vsv_vrange_vsubset_vifunion_app:
assumes "𝒟⇩∘ r = I" and "⋀i. i ∈⇩∘ I ⟹ r⦇i⦈ ∈⇩∘ A i"
shows "ℛ⇩∘ r ⊆⇩∘ (⋃⇩∘i∈⇩∘I. A i)"
proof(intro vsubsetI)
fix x assume "x ∈⇩∘ ℛ⇩∘ r"
with assms(1) obtain i where x_def: "x = r⦇i⦈" and i: "i ∈⇩∘ I"
by (metis vrange_atE)
from i assms(2)[rule_format, OF i] show "x ∈⇩∘ (⋃⇩∘i∈⇩∘I. A i)"
unfolding x_def by (intro vifunionI) auto
qed

lemma v11_vlrestriction_vifintersection:
assumes "I ≠ 0" and "⋀i. i ∈⇩∘ I ⟹ v11 (f ↾⇧l⇩∘ (A i))"
shows "v11 (f ↾⇧l⇩∘ (⋂⇩∘i∈⇩∘I. A i))"
proof(intro v11I)
show "vsv (f ↾⇧l⇩∘ ⋂⇩∘ ((λa∈⇩∘I. A a) `⇩∘ I))"
(*slow*)
apply(subgoal_tac ‹⋀i. i ∈⇩∘ I ⟹ vsv (f ↾⇧l⇩∘ (A i))›)
subgoal by (insert assms(1), intro vsvI) (blast intro!: vsubset_antisym)+
subgoal using assms by blast
done
show "vsv ((f ↾⇧l⇩∘ ⋂⇩∘ ((λa∈⇩∘I. A a) `⇩∘ I))¯⇩∘)"
proof(intro vsvI)
fix a b c
assume ab: "⟨a, b⟩ ∈⇩∘ (f ↾⇧l⇩∘ ⋂⇩∘ ((λa∈⇩∘I. A a) `⇩∘ I))¯⇩∘"
and ac: "⟨a, c⟩ ∈⇩∘ (f ↾⇧l⇩∘ ⋂⇩∘ ((λa∈⇩∘I. A a) `⇩∘ I))¯⇩∘"
from assms(2) have hyp: "⋀i. i ∈⇩∘ I ⟹ vsv ((f ↾⇧l⇩∘ (A i))¯⇩∘)" by blast
from assms(1) obtain i where "i ∈⇩∘ I" and "⋂⇩∘ ((λa∈⇩∘I. A a) `⇩∘ I) ⊆⇩∘ A i"
by (auto intro!: vsubset_antisym)
with ab ac hyp ‹i ∈⇩∘ I› show "b = c" by auto
qed auto
qed

subsection‹Additional simplification rules for indexed families of sets.›

text‹Union.›

lemma vifunion_simps[simp]:
"⋀a B I. (⋃⇩∘i∈⇩∘I. vinsert a (B i)) =
(if I=0 then 0 else vinsert a (⋃⇩∘i∈⇩∘I. B i))"
"⋀A B I. (⋃⇩∘i∈⇩∘I. A i ∪⇩∘ B) = ((if I=0 then 0 else (⋃⇩∘i∈⇩∘I. A i) ∪⇩∘ B))"
"⋀A B I. (⋃⇩∘i∈⇩∘I. A ∪⇩∘ B i) = ((if I=0 then 0 else A ∪⇩∘ (⋃⇩∘i∈⇩∘I. B i)))"
"⋀A B I. (⋃⇩∘i∈⇩∘I. A i ∩⇩∘ B) = ((⋃⇩∘i∈⇩∘I. A i) ∩⇩∘ B)"
"⋀A B I. (⋃⇩∘i∈⇩∘I. A ∩⇩∘ B i) = (A ∩⇩∘ (⋃⇩∘i∈⇩∘I. B i))"
"⋀A B I. (⋃⇩∘i∈⇩∘I. A i -⇩∘ B) = ((⋃⇩∘i∈⇩∘I. A i) -⇩∘ B)"
"⋀A B. (⋃⇩∘i∈⇩∘⋃⇩∘A. B i) = (⋃⇩∘y∈⇩∘A. ⋃⇩∘i∈⇩∘y. B i)"
by
(
force
simp: vrange_VLambda vimage_VLambda_vrange_rep
intro!: vsubset_antisym
)+

lemma vifunion_simps_ext:
"⋀a B I. vinsert a (⋃⇩∘i∈⇩∘I. B i) =
(if I=0 then set {a} else (⋃⇩∘i∈⇩∘I. vinsert a (B i)))"
"⋀A B I. (⋃⇩∘i∈⇩∘I. A i) ∪⇩∘ B = (if I=0 then B else (⋃⇩∘i∈⇩∘I. A i ∪⇩∘ B))"
"⋀A B I. A ∪⇩∘ (⋃⇩∘i∈⇩∘I. B i) = (if I=0 then A else (⋃⇩∘i∈⇩∘I. A ∪⇩∘ B i))"
"⋀A B I. ((⋃⇩∘i∈⇩∘I. A i) ∩⇩∘ B) = (⋃⇩∘i∈⇩∘I. A i ∩⇩∘ B)"
"⋀A B I. ((⋃⇩∘i∈⇩∘I. A i) -⇩∘ B) = (⋃⇩∘i∈⇩∘I. A i -⇩∘ B)"
"⋀A B. (⋃⇩∘y∈⇩∘A. ⋃⇩∘i∈⇩∘y. B i) = (⋃⇩∘i∈⇩∘⋃⇩∘A. B i)"
by (auto simp: vrange_VLambda)

lemma vifunion_vball_vbex_simps[simp]:
"⋀A P. (∀a∈⇩∘⋃⇩∘A. P a) ⟷ (∀y∈⇩∘A. ∀a∈⇩∘y. P a)"
"⋀A P. (∃a∈⇩∘⋃⇩∘A. P a) ⟷ (∃y∈⇩∘A. ∃a∈⇩∘y. P a)"
using vball_vifunion vbex_vifunion by auto

text‹Intersection.›

lemma vifintersection_simps[simp]:
"⋀I A B. (⋂⇩∘i∈⇩∘I. A i ∩⇩∘ B) = (if I = 0 then 0 else (⋂⇩∘i∈⇩∘I. A i) ∩⇩∘ B)"
"⋀I A B. (⋂⇩∘i∈⇩∘I. A ∩⇩∘ B i) = (if I = 0 then 0 else A ∩⇩∘ (⋂⇩∘i∈⇩∘I. B i))"
"⋀I A B. (⋂⇩∘i∈⇩∘I. A i -⇩∘ B) = (if I = 0 then 0 else (⋂⇩∘i∈⇩∘I. A i) -⇩∘ B)"
"⋀I A B. (⋂⇩∘i∈⇩∘I. A -⇩∘ B i) = (if I = 0 then 0 else A -⇩∘ (⋃⇩∘i∈⇩∘I. B i))"
"⋀I a B.
(⋂⇩∘i∈⇩∘I. vinsert a (B i)) = (if I = 0 then 0 else vinsert a (⋂⇩∘i∈⇩∘I. B i))"
"⋀I A B. (⋂⇩∘i∈⇩∘I. A i ∪⇩∘ B) = (if I = 0 then 0 else ((⋂⇩∘i∈⇩∘I. A i) ∪⇩∘ B))"
"⋀I A B. (⋂⇩∘i∈⇩∘I. A ∪⇩∘ B i) = (if I = 0 then 0 else (A ∪⇩∘ (⋂⇩∘i∈⇩∘I. B i)))"
by force+

lemma vifintersection_simps_ext:
"⋀A B I. (⋂⇩∘i∈⇩∘I. A i) ∩⇩∘ B = (if I = 0 then 0 else (⋂⇩∘i∈⇩∘I. A i ∩⇩∘ B))"
"⋀A B I. A ∩⇩∘ (⋂⇩∘i∈⇩∘I. B i) = (if I = 0 then 0 else (⋂⇩∘i∈⇩∘I. A ∩⇩∘ B i))"
"⋀A B I. (⋂⇩∘i∈⇩∘I. A i) -⇩∘ B = (if I = 0 then 0 else (⋂⇩∘i∈⇩∘I. A i -⇩∘ B))"
"⋀A B I. A -⇩∘ (⋃⇩∘i∈⇩∘I. B i) = (if I = 0 then A else (⋂⇩∘i∈⇩∘I. A -⇩∘ B i))"
"⋀a B I. vinsert a (⋂⇩∘i∈⇩∘I. B i) =
(if I = 0 then set {a} else (⋂⇩∘i∈⇩∘I. vinsert a (B i)))"
"⋀A B I. ((⋂⇩∘i∈⇩∘I. A i) ∪⇩∘ B) = (if I = 0 then B else (⋂⇩∘i∈⇩∘I. A i ∪⇩∘ B))"
"⋀A B I. A ∪⇩∘ (⋂⇩∘i∈⇩∘I. B i) = (if I = 0 then A else (⋂⇩∘i∈⇩∘I. A ∪⇩∘ B i))"
using vifintersection_simps by auto

subsection‹Knowledge transfer: union and intersection of indexed families›

lemma SUP_vifunion: "(SUP ξ∈elts α. A ξ) = (⋃⇩∘ξ∈⇩∘α. A ξ)"
by (simp add: vimage_VLambda_vrange_rep vrange_VLambda)

lemma INF_vifintersection: "(INF ξ∈elts α. A ξ) = (⋂⇩∘ξ∈⇩∘α. A ξ)"
by (simp add: vimage_VLambda_vrange_rep vrange_VLambda)

lemmas Ord_induct3'[consumes 1, case_names 0 succ Limit, induct type: V] =
Ord_induct3[unfolded SUP_vifunion]

lemma Limit_vifunion_def[simp]:
assumes "Limit α"
shows "(⋃⇩∘ξ∈⇩∘α. ξ) = α"
using assms unfolding SUP_vifunion[symmetric] by simp

lemmas_with[unfolded SUP_vifunion INF_vifintersection]:
TC = ZFC_Cardinals.TC
and rank_Sup = ZFC_Cardinals.rank_Sup
and TC_def = ZFC_Cardinals.TC_def
and Ord_equality = ZFC_in_HOL.Ord_equality
and Aleph_Limit = ZFC_Cardinals.Aleph_Limit
and rank = ZFC_Cardinals.rank
and Vset = ZFC_in_HOL.Vset
and mult = Kirby.mult
and Aleph_def = ZFC_Cardinals.Aleph_def
and times_V_def = Kirby.times_V_def
and mult_Limit = Kirby.mult_Limit
and Vfrom = ZFC_in_HOL.Vfrom
and Vfrom_def = ZFC_in_HOL.Vfrom_def
and rank_def = ZFC_Cardinals.rank_def
and Limit_Vfrom_eq = ZFC_in_HOL.Limit_Vfrom_eq
and VSigma_def = ZFC_Cardinals.VSigma_def
and TC_mult = Kirby.TC_mult

subsection‹Disjoint union›

text‹
See the main library of ‹ZFC in HOL› for further information
and elementary properties.
›

syntax "_VSIGMA" :: "pttrn ⇒ V ⇒ V ⇒ V" (‹(3∐⇩∘_∈⇩∘_./ _)› [0, 0, 10] 10)

translations "∐⇩∘i∈⇩∘I. A" ⇌ "CONST VSigma I (λi. A)"

text‹Further rules.›

lemma vdunion_def: "(∐⇩∘i∈⇩∘I. A i) = (⋃⇩∘i∈⇩∘I. ⋃⇩∘x∈⇩∘A i. set {⟨i, x⟩})"
by (auto simp: vrange_VLambda vimage_VLambda_vrange_rep)

lemma vdunionI:
assumes "ix = ⟨i, x⟩" and "i ∈⇩∘ I" and "x ∈⇩∘ A i"
shows "ix ∈⇩∘ (∐⇩∘i∈⇩∘I. A i)"
using assms(2,3) unfolding assms(1) vdunion_def by (intro vifunionI) auto

and vdunionE = VSigmaE

text‹Set operations.›

lemma vdunion_vsingleton: "(∐⇩∘i∈⇩∘set{c}. A i) = set {c} ×⇩∘ A c" by auto

lemma vdunion_vdoubleton:
"(∐⇩∘i∈⇩∘set{a, b}. A i) = set {a} ×⇩∘ A a ∪⇩∘ set {b} ×⇩∘ A b"
by auto

text‹Connections.›

lemma vdunion_vsum: "(∐⇩∘i∈⇩∘set{0, 1}. if i=0 then A else B) = A ⨄ B"
unfolding vdunion_vdoubleton vsum_def by simp

subsection‹Canonical injection›

definition vcinjection :: "(V ⇒ V) ⇒ V ⇒ V"
where "vcinjection A i = (λx∈⇩∘A i. ⟨i, x⟩)"

text‹Rules.›

mk_VLambda vcinjection_def
|vsv vcinjection_vsv[intro]|
|vdomain vcinjection_vdomain[simp]|
|app vcinjection_app[simp, intro]|

text‹Elementary results.›

lemma vcinjection_vrange_vsubset:
assumes "i ∈⇩∘ I"
shows "ℛ⇩∘ (vcinjection A i) ⊆⇩∘ (∐⇩∘i∈⇩∘I. A i)"
unfolding vcinjection_def
proof(intro vrange_VLambda_vsubset)
fix x assume prems: "x ∈⇩∘ A i"
show "⟨i, x⟩ ∈⇩∘ (∐⇩∘i∈⇩∘I. A i)"
by (intro vdunionI[where A=A, OF _ assms prems]) simp
qed

lemma vcinjection_vrange:
assumes "i ∈⇩∘ I" and "⋀j. j ∈⇩∘ I ⟹ A j ≠ 0"
shows "ℛ⇩∘ (vcinjection A i) = (⋃⇩∘x∈⇩∘A i. set {⟨i, x⟩})"
proof(intro vsubset_antisym)
interpret vsv ‹vcinjection A i› by (rule vcinjection_vsv)
show "ℛ⇩∘ (vcinjection A i) ⊆⇩∘ (⋃⇩∘x∈⇩∘A i. set {⟨i, x⟩})"
unfolding vcinjection_def
proof(intro vrange_VLambda_vsubset)
fix x assume prems: "x ∈⇩∘ A i"
show "⟨i, x⟩ ∈⇩∘ (⋃⇩∘x∈⇩∘A i. set {⟨i, x⟩})"
by (intro vifunionI, rule prems) simp
qed
show "(⋃⇩∘x∈⇩∘A i. set {⟨i, x⟩}) ⊆⇩∘ ℛ⇩∘ (vcinjection A i)"
proof(rule vsubsetI)
fix ix assume "ix ∈⇩∘ (⋃⇩∘x∈⇩∘A i. set {⟨i, x⟩})"
then obtain x where x: "x ∈⇩∘ A i" and ix_def: "ix = ⟨i, x⟩"
by (elim vifunionE) auto
with x show "ix ∈⇩∘ ℛ⇩∘ (vcinjection A i)"
unfolding ix_def by (intro vsv_vimageI2') auto
qed
qed

subsection‹Infinite Cartesian product›

definition vproduct :: "V ⇒ (V ⇒ V) ⇒ V"
where "vproduct I A = set {f. vsv f ∧ 𝒟⇩∘ f = I ∧ (∀i∈⇩∘I. f⦇i⦈ ∈⇩∘ A i)}"

syntax "_VPRODUCT" :: "pttrn ⇒ V ⇒ V ⇒ V" (‹(3∏⇩∘_∈⇩∘_./ _)› [0, 0, 10] 10)

translations "∏⇩∘i∈⇩∘I. A" ⇌ "CONST vproduct I (λi. A)"

lemma small_vproduct[simp]:
"small {f. vsv f ∧ 𝒟⇩∘ f = I ∧ (∀i∈⇩∘I. f⦇i⦈ ∈⇩∘ A i)}"
(is ‹small ?A›)
proof-
from small_vsv[of I ‹(⋃⇩∘i∈⇩∘I. A i)›] have
"small {f. vsv f ∧ 𝒟⇩∘ f = I ∧ ℛ⇩∘ f ⊆⇩∘ (⋃⇩∘i∈⇩∘I. A i)}"
by simp
moreover have "?A ⊆ {f. vsv f ∧ 𝒟⇩∘ f = I ∧ ℛ⇩∘ f ⊆⇩∘ (⋃⇩∘i∈⇩∘I. A i)}"
proof(intro subsetI, unfold mem_Collect_eq, elim conjE, intro conjI)
fix f assume prems: "vsv f" "𝒟⇩∘ f = I" "∀i∈elts I. f⦇i⦈ ∈⇩∘ A i"
interpret vsv f by (rule prems(1))
show "ℛ⇩∘ f ⊆⇩∘ (⋃⇩∘i∈⇩∘I. A i)"
proof(intro vsubsetI)
fix y assume "y ∈⇩∘ ℛ⇩∘ f"
with prems(2) obtain i where y_def: "y = f⦇i⦈" and i: "i ∈⇩∘ I"
by (blast dest: vrange_atD)
from i prems(3) vifunionI show "y ∈⇩∘ (⋃⇩∘i∈⇩∘I. A i)"
unfolding y_def by auto
qed
qed
ultimately show ?thesis by (metis (lifting) smaller_than_small)
qed

text‹Rules.›

lemma vproductI[intro!]:
assumes "vsv f" and "𝒟⇩∘ f = I" and "∀i∈⇩∘I. f⦇i⦈ ∈⇩∘ A i"
shows "f ∈⇩∘ (∏⇩∘i∈⇩∘I. A i)"
using assms small_vproduct unfolding vproduct_def by auto

lemma vproductD[dest]:
assumes "f ∈⇩∘ (∏⇩∘i∈⇩∘I. A i)"
shows "vsv f"
and "𝒟⇩∘ f = I"
and "∀i∈⇩∘I. f⦇i⦈ ∈⇩∘ A i"
using assms unfolding vproduct_def by auto

lemma vproductE[elim!]:
assumes "f ∈⇩∘ (∏⇩∘i∈⇩∘I. A i)"
obtains "vsv f" and "𝒟⇩∘ f = I" and "∀i∈⇩∘I. f⦇i⦈ ∈⇩∘ A i"
using assms unfolding vproduct_def by auto

text‹Set operations.›

lemma vproduct_index_vempty[simp]: "(∏⇩∘i∈⇩∘0. A i) = set {0}"
proof-
have "{f. vsv f ∧ 𝒟⇩∘ f = 0 ∧ (∀i∈⇩∘0. f⦇i⦈ ∈⇩∘ A i)} = {0}"
using vbrelation.vlrestriction_vdomain vsv_eqI by fastforce
then show ?thesis unfolding vproduct_def by simp
qed

lemma vproduct_vsingletonI:
assumes "f⦇c⦈ ∈⇩∘ A c" and "f = set {⟨c, f⦇c⦈⟩}"
shows "f ∈⇩∘ (∏⇩∘i∈⇩∘set{c}. A i)"
using assms
apply(intro vproductI)
subgoal by (metis rel_vsingleton.vsv_axioms)
subgoal by (force intro!: vsubset_antisym)
subgoal by auto
done

lemma vproduct_vsingletonD:
assumes "f ∈⇩∘ (∏⇩∘i∈⇩∘set{c}. A i)"
shows "vsv f" and "f⦇c⦈ ∈⇩∘ A c" and "f = set {⟨c, f⦇c⦈⟩}"
proof-
from assms show "f = set {⟨c, f⦇c⦈⟩}"
by (elim vproductE) (metis VLambda_vsingleton  vsv.vsv_is_VLambda)
qed (use assms in auto)

lemma vproduct_vsingletonE:
assumes "f ∈⇩∘ (∏⇩∘i∈⇩∘set{c}. A i)"
obtains "vsv f" and "f⦇c⦈ ∈⇩∘ A c" and "f = set {⟨c, f⦇c⦈⟩}"
using assms vproduct_vsingletonD that by auto

lemma vproduct_vsingleton_iff:
"f ∈⇩∘ (∏⇩∘i∈⇩∘set{c}. A i) ⟷ f⦇c⦈ ∈⇩∘ A c ∧ f = set {⟨c, f⦇c⦈⟩}"
by (rule iffI) (auto simp: vproduct_vsingletonD intro!: vproduct_vsingletonI)

lemma vproduct_vdoubletonI[intro]:
assumes "vsv f"
and "f⦇a⦈ ∈⇩∘ A a"
and "f⦇b⦈ ∈⇩∘ A b"
and "𝒟⇩∘ f = set {a, b}"
and "ℛ⇩∘ f ⊆⇩∘ A a ∪⇩∘ A b"
shows "f ∈⇩∘ (∏⇩∘i∈⇩∘set {a, b}. A i)"
using assms vifunion_vdoubleton by (intro vproductI) auto

lemma vproduct_vdoubletonD[dest]:
assumes "f ∈⇩∘ (∏⇩∘i∈⇩∘set{a, b}. A i)"
shows "vsv f"
and "f⦇a⦈ ∈⇩∘ A a"
and "f⦇b⦈ ∈⇩∘ A b"
and "𝒟⇩∘ f = set {a, b}"
and "f = set {⟨a, f⦇a⦈⟩, ⟨b, f⦇b⦈⟩}"
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms vifunion_vdoubleton by fastforce
subgoal by (metis assms VLambda_vdoubleton vproductE vsv.vsv_is_VLambda)
done

lemma vproduct_vdoubletonE:
assumes "f ∈⇩∘ (∏⇩∘i∈⇩∘set{a, b}. A i)"
obtains "vsv f"
and "f⦇a⦈ ∈⇩∘ A a"
and "f⦇b⦈ ∈⇩∘ A b"
and "𝒟⇩∘ f = set {a, b}"
and "f = set {⟨a, f⦇a⦈⟩, ⟨b, f⦇b⦈⟩}"
using assms vproduct_vdoubletonD that by simp

lemma vproduct_vdoubleton_iff:
"f ∈⇩∘ (∏⇩∘i∈⇩∘set {a, b}. A i) ⟷
vsv f ∧
f⦇a⦈ ∈⇩∘ A a ∧
f⦇b⦈ ∈⇩∘ A b ∧
𝒟⇩∘ f = set {a, b} ∧
f = set {⟨a, f⦇a⦈⟩, ⟨b, f⦇b⦈⟩}"
by (force elim!: vproduct_vdoubletonE)+

text‹Elementary properties.›

lemma vproduct_eq_vemptyI:
assumes "i ∈⇩∘ I" and "A i = 0"
shows "(∏⇩∘i∈⇩∘I. A i) = 0"
proof(intro vsubset_antisym vsubsetI)
fix x assume prems: "x ∈⇩∘ (∏⇩∘i∈⇩∘I. A i)"
from assms vproductD(3)[OF prems] show "x ∈⇩∘ 0" by auto
qed auto

lemma vproduct_eq_vemptyD:
assumes "(∏⇩∘i∈⇩∘I. A i) ≠ 0"
shows "⋀i. i ∈⇩∘ I ⟹ A i ≠ 0"
proof(rule ccontr, unfold not_not)
fix i assume prems: "i ∈⇩∘ I" "A i = 0"
with vproduct_eq_vemptyI[where A=A, OF prems] assms show False by simp
qed

lemma vproduct_vrange:
assumes "f ∈⇩∘ (∏⇩∘i∈⇩∘I. A i)"
shows "ℛ⇩∘ f ⊆⇩∘ (⋃⇩∘i∈⇩∘I. A i)"
proof(intro vsubsetI)
fix x assume prems: "x ∈⇩∘ ℛ⇩∘ f"
have vsv_f: "vsv f"
and dom_f: "𝒟⇩∘ f = I"
and fi: "⋀i. i ∈⇩∘ I ⟹ f⦇i⦈ ∈⇩∘ A i"
by (simp_all add: vproductD[OF assms, rule_format])
interpret f: vsv f by (rule vsv_f)
from prems dom_f obtain i where x_def: "x = f⦇i⦈" and i: "i ∈⇩∘ I"
by (auto elim: f.vrange_atE)
from i fi show "x ∈⇩∘ (⋃⇩∘i∈⇩∘I. A i)" unfolding x_def by (intro vifunionI) auto
qed

lemma vproduct_vsubset_VPow: "(∏⇩∘i∈⇩∘I. A i) ⊆⇩∘ VPow (I ×⇩∘ (⋃⇩∘i∈⇩∘I. A i))"
proof(intro vsubsetI)
fix f assume "f ∈⇩∘ (∏⇩∘i∈⇩∘I. A i)"
then have vsv: "vsv f"
and domain: "𝒟⇩∘ f = I"
and range: "∀i∈elts I. f⦇i⦈ ∈⇩∘ A i"
by auto
interpret f: vsv f by (rule vsv)
have "f ⊆⇩∘ I ×⇩∘ (⋃⇩∘i∈⇩∘I. A i)"
proof(intro vsubsetI)
fix x assume prems: "x ∈⇩∘ f"
then obtain a b where x_def: "x = ⟨a, b⟩" by (elim f.vbrelation_vinE)
with prems have "a ∈⇩∘ 𝒟⇩∘ f" and "b ∈⇩∘ ℛ⇩∘ f" by auto
with range domain prems show "x ∈⇩∘ I ×⇩∘ (⋃⇩∘i∈⇩∘I. A i)"
by (fastforce simp: x_def)
qed
then show "f ∈⇩∘ VPow (I ×⇩∘ (⋃⇩∘i∈⇩∘I. A i))" by simp
qed

lemma VLambda_in_vproduct:
assumes "⋀i. i ∈⇩∘ I ⟹ f i ∈⇩∘ A i"
shows "(λi∈⇩∘I. f i) ∈⇩∘ (∏⇩∘i∈⇩∘I. A i)"
using assms by (simp add: vproductI vsv.vsv_vrange_vsubset_vifunion_app)

lemma vproduct_cong:
assumes "⋀i. i ∈⇩∘ I ⟹ f i = g i"
shows "(∏⇩∘i∈⇩∘I. f i) = (∏⇩∘i∈⇩∘I. g i)"
proof-
have "(∏⇩∘i∈⇩∘I. f i) ⊆⇩∘ (∏⇩∘i∈⇩∘I. g i)" if "⋀i. i ∈⇩∘ I ⟹ f i = g i" for f g
proof(intro vsubsetI)
fix x assume "x ∈⇩∘ (∏⇩∘i∈⇩∘I. f i)"
note xD = vproductD[OF this]
interpret vsv x by (rule xD(1))
show "x ∈⇩∘ (∏⇩∘i∈⇩∘I. g i)"
by (metis xD(2,3) that VLambda_in_vproduct vsv_is_VLambda)
qed
with assms show ?thesis by (intro vsubset_antisym) auto
qed

lemma vproduct_ex_in_vproduct:
assumes "x ∈⇩∘ (∏⇩∘i∈⇩∘J. A i)" and "J ⊆⇩∘ I" and "⋀i. i ∈⇩∘ I ⟹ A i ≠ 0"
obtains X where "X ∈⇩∘ (∏⇩∘i∈⇩∘I. A i)" and "x = X ↾⇧l⇩∘ J"
proof-
define X where "X = (λi∈⇩∘I. if i ∈⇩∘ J then x⦇i⦈ else (SOME x. x ∈⇩∘ A i))"
have X: "X ∈⇩∘ (∏⇩∘i∈⇩∘I. A i)"
by (intro vproductI) (use assms in ‹auto simp: X_def›)
moreover have "x = X ↾⇧l⇩∘ J"
proof(rule vsv_eqI)
from assms(1) have [simp]: "𝒟⇩∘ x = J" by clarsimp
moreover from assms(2) have "𝒟⇩∘ (X ↾⇧l⇩∘ J) = J" unfolding X_def by fastforce
ultimately show "𝒟⇩∘ x = 𝒟⇩∘ (X ↾⇧l⇩∘ J)" by simp
show "x⦇i⦈ = (X ↾⇧l⇩∘ J)⦇i⦈" if "i ∈⇩∘ 𝒟⇩∘ x" for i
using that assms(2) unfolding X_def by auto
qed (use assms X in auto)
ultimately show ?thesis using that by simp
qed

lemma vproduct_vsingleton_def: "(∏⇩∘i∈⇩∘set {j}. A i) = (∏⇩∘i∈⇩∘set {j}. A j)"
by auto

lemma vprojection_in_VUnionI:
assumes "A ⊆⇩∘ (∏⇩∘i∈⇩∘I. F i)" and "f ∈⇩∘ A" and "i ∈⇩∘ I"
shows "f⦇i⦈ ∈⇩∘ ⋃⇩∘(⋃⇩∘(⋃⇩∘A))"
proof(intro VUnionI)
show "f ∈⇩∘ A" by (rule assms(2))
from assms(1,2) have "f ∈⇩∘ (∏⇩∘i∈⇩∘I. F i)" by auto
note f = vproductD[OF this, rule_format]
interpret vsv f rewrites "𝒟⇩∘ f = I" by (auto intro: f(1) simp: f(2))
show "⟨i, f⦇i⦈⟩ ∈⇩∘ f" by (meson assms(3) vsv_appE)
show "set {i, f⦇i⦈} ∈⇩∘ ⟨i, f⦇i⦈⟩" unfolding vpair_def by simp
qed simp

subsection‹Projection›

definition vprojection :: "V ⇒ (V ⇒ V) ⇒ V ⇒ V"
where "vprojection I A i = (λf∈⇩∘(∏⇩∘i∈⇩∘I. A i). f⦇i⦈)"

text‹Rules.›

mk_VLambda vprojection_def
|vsv vprojection_vsv[intro]|
|vdomain vprojection_vdomain[simp]|
|app vprojection_app[simp, intro]|

text‹Elementary results.›

lemma vprojection_vrange_vsubset:
assumes "i ∈⇩∘ I"
shows "ℛ⇩∘ (vprojection I A i) ⊆⇩∘ A i"
unfolding vprojection_def
proof(intro vrange_VLambda_vsubset)
fix f assume prems: "f ∈⇩∘ (∏⇩∘i∈⇩∘I. A i)"
show "f⦇i⦈ ∈⇩∘ A i" by (intro vproductD(3)[OF prems, rule_format] assms)
qed

lemma vprojection_vrange:
assumes "i ∈⇩∘ I" and "⋀j. j ∈⇩∘ I ⟹ A j ≠ 0"
shows "ℛ⇩∘ (vprojection I A i) = A i"
proof
(
intro
vsubset_antisym vprojection_vrange_vsubset vrange_VLambda_vsubset assms(1)
)
show "A i ⊆⇩∘ ℛ⇩∘ (vprojection I A i)"
proof(intro vsubsetI)
fix x assume prems: "x ∈⇩∘ A i"
obtain f
where f: "⋀x. x ∈⇩∘ set {A i | i. i ∈⇩∘ I} ⟹ x ≠ 0 ⟹ f⦇x⦈ ∈⇩∘ x"
and "vsv f"
using that by (rule Axiom_of_Choice)
define f' where "f' = (λj∈⇩∘I. if j = i then x else f⦇A j⦈)"
show "x ∈⇩∘ ℛ⇩∘ (vprojection I A i)"
unfolding vprojection_def
proof(rule rel_VLambda.vsv_vimageI2')
show "f' ∈⇩∘ 𝒟⇩∘ (λf∈⇩∘vproduct I A. f⦇i⦈)"
unfolding vdomain_VLambda
proof(intro vproductI, unfold Ball_def; (intro allI conjI impI)?)
fix j assume "j ∈⇩∘ I"
with prems assms(2) show "f'⦇j⦈ ∈⇩∘ A j"
unfolding f'_def by (cases ‹j = i›) (auto intro!: f)
qed (simp_all add: f'_def)
with assms(1) show "x = (λf∈⇩∘vproduct I A. f⦇i⦈)⦇f'⦈"
unfolding f'_def by simp
qed
qed
qed

subsection‹Cartesian power of a set›

definition vcpower :: "V ⇒ V ⇒ V" (infixr ‹^⇩×› 80)
where "A ^⇩× n = (∏⇩∘i∈⇩∘n. A)"

text‹Rules.›

lemma vcpowerI[intro]:
assumes "f ∈⇩∘ (∏⇩∘i∈⇩∘n. A)"
shows "f ∈⇩∘ (A ^⇩× n)"
using assms unfolding vcpower_def by auto

lemma vcpowerD[dest]:
assumes "f ∈⇩∘ (A ^⇩× n)"
shows "f ∈⇩∘ (∏⇩∘i∈⇩∘n. A)"
using assms unfolding vcpower_def by auto

lemma vcpowerE[elim]:
assumes "f ∈⇩∘ (A ^⇩× n)" and "f ∈⇩∘ (∏⇩∘i∈⇩∘n. A) ⟹ P"
shows P
using assms unfolding vcpower_def by auto

text‹Set operations.›

lemma vcpower_index_vempty[simp]: "A ^⇩× 0 = set {0}"
unfolding vcpower_def by (rule vproduct_index_vempty)

lemma vcpower_of_vempty:
assumes "n ≠ 0"
shows "0 ^⇩× n = 0"
using assms unfolding vcpower_def vproduct_def by simp

lemma vcpower_vsubset_mono:
assumes "A ⊆⇩∘ B"
shows "A ^⇩× n ⊆⇩∘ B ^⇩× n"
using assms
by (intro vsubsetI vcpowerI vproductI)
(auto intro: vproductD[OF vcpowerD, rule_format])

text‹Connections.›

lemma vcpower_vdomain:
assumes "f ∈⇩∘ (A ^⇩× n)"
shows "𝒟⇩∘ f = n"
using assms by auto

lemma vcpower_vrange:
assumes "f ∈⇩∘ (A ^⇩× n)"
shows "ℛ⇩∘ f ⊆⇩∘ A"
using assms by (intro vsubsetI; elim vcpowerE vproductE) auto

text‹\newpage›

end```