Images and preimages of sets #
Main definitions #
-
preimage f t : Set α
: the preimage f⁻¹(t) (writtenf ⁻¹' t
in Lean) of a subset of β. -
range f : Set β
: the image ofuniv
underf
. Also works for{p : Prop} (f : p → α)
(unlikeimage
)
Notation #
-
f ⁻¹' t
forSet.preimage f t
-
f '' s
forSet.image f s
Tags #
set, sets, image, preimage, pre-image, range
Inverse image #
f ⁻¹' t
denotes the preimage of t : Set β
under the function f : α → β
.
Instances For
Image of a set under a function #
f '' s
denotes the image of s : Set α
under the function f : α → β
.
Instances For
A common special case of image_congr
Set.image
is monotone. See Set.image_subset
for the statement in terms of ⊆
.
Restriction of f
to s
factors through s.imageFactorization f : s → f '' s
.
Instances For
If the only elements outside s
are those left fixed by σ
, then mapping by σ
has no effect.
Lemmas about the powerset and image. #
Lemmas about range of a function. #
Alias of the reverse direction of Set.range_iff_surjective
.
Any map f : ι → β
factors through a map rangeFactorization f : ι → range f
.
Instances For
The image of a subsingleton is a subsingleton.
The preimage of a subsingleton under an injective map is a subsingleton.
If the image of a set under an injective map is a subsingleton, the set is a subsingleton.
If the preimage of a set under a surjective map is a subsingleton, the set is a subsingleton.
The preimage of a nontrivial set under a surjective map is nontrivial.
The image of a nontrivial set under an injective map is nontrivial.
If the image of a set is nontrivial, the set is nontrivial.
If the preimage of a set under an injective map is nontrivial, the set is nontrivial.