# Theory Basic

```section ‹Basics›

theory Basic
imports Main
begin

subsection ‹Miscellaneous›

abbreviation (input) "const x ≡ λ _. x"

lemmas [simp] = map_prod.id map_prod.comp[symmetric]
lemma prod_UNIV[iff]: "A × B = UNIV ⟷ A = UNIV ∧ B = UNIV" by auto
lemma prod_singleton:
"fst ` A = {x} ⟹ A = fst ` A × snd ` A"
"snd ` A = {y} ⟹ A = fst ` A × snd ` A"
by force+

lemma infinite_subset[trans]: "infinite A ⟹ A ⊆ B ⟹ infinite B" using infinite_super by this
lemma finite_subset[trans]: "A ⊆ B ⟹ finite B ⟹ finite A" using finite_subset by this

declare infinite_coinduct[case_names infinite, coinduct pred: infinite]
lemma infinite_psubset_coinduct[case_names infinite, consumes 1]:
assumes "R A"
assumes "⋀ A. R A ⟹ ∃ B ⊂ A. R B"
shows "infinite A"
proof
show "False" if "finite A" using that assms by (induct rule: finite_psubset_induct) (auto)
qed

(* TODO: why are there two copies of this theorem? *)
thm inj_on_subset subset_inj_on

lemma inj_inj_on[dest]: "inj f ⟹ inj_on f S" using inj_on_subset by auto

end
```