Equivalences and sets #
In this file we provide lemmas linking equivalences to sets.
Some notable definitions are:
Equiv.ofInjective
: an injective function is (noncomputably) equivalent to its range.Equiv.setCongr
: two equal sets are equivalent as types.Equiv.Set.union
: a disjoint union of sets is equivalent to theirSum
.
This file is separate from Equiv/Basic
such that we do not require the full lattice structure
on sets before defining what an equivalence is.
Alias for Equiv.image_eq_preimage
Alias for Equiv.image_eq_preimage
An empty set is equivalent to a PEmpty
type.
Instances For
If a ∉ s
, then insert a s
is equivalent to s ⊕ PUnit
.
Instances For
If s : Set α
is a set with decidable membership, then s ⊕ sᶜ
is equivalent to α
.
Instances For
sumDiffSubset s t
is the natural equivalence between
s ⊕ (t \ s)
and t
, where s
and t
are two sets.
Instances For
Given an equivalence e₀
between sets s : Set α
and t : Set β
, the set of equivalences
e : α ≃ β
such that e ↑x = ↑(e₀ x)
for each x : s
is equivalent to the set of equivalences
between sᶜ
and tᶜ
.
Instances For
If f
is an injective function, then s
is equivalent to f '' s
.
Instances For
If s
is a set in range f
,
then its image under rangeSplitting f
is in bijection (via f
) with s
.
Instances For
If f : α → β
has a left-inverse when α
is nonempty, then α
is computably equivalent to the
range of f
.
While awkward, the Nonempty α
hypothesis on f_inv
and hf
allows this to be used when α
is
empty too. This hypothesis is absent on analogous definitions on stronger Equiv
s like
LinearEquiv.ofLeftInverse
and RingEquiv.ofLeftInverse
as their typeclass assumptions
are already sufficient to ensure non-emptiness.
Instances For
If f : α → β
has a left-inverse, then α
is computably equivalent to the range of f
.
Note that if α
is empty, no such f_inv
exists and so this definition can't be used, unlike
the stronger but less convenient ofLeftInverse
.
Instances For
If f : α → β
is an injective function, then domain α
is equivalent to the range of f
.
Instances For
sigmaPreimageEquiv f
for f : α → β
is the natural equivalence between
the type of all preimages of points under f
and the total space α
.
Instances For
The composition of an updated function with an equiv on a subtype can be expressed as an updated function.