Functions over sets #
Main definitions #
Predicate #
Set.EqOn f₁ f₂ s: functionsf₁andf₂are equal at every point ofs;Set.MapsTo f s t:fsends every point ofsto a point oft;Set.InjOn f s: restriction offtosis injective;Set.SurjOn f s t: every point inshas a preimage ins;Set.BijOn f s t:fis a bijection betweensandt;Set.LeftInvOn f' f s: for everyx ∈ swe havef' (f x) = x;Set.RightInvOn f' f t: for everyy ∈ twe havef (f' y) = y;Set.InvOn f' f s t:f'is a two-side inverse offonsandt, i.e. we haveSet.LeftInvOn f' f sandSet.RightInvOn f' f t.
Functions #
Set.restrict f s: restrict the domain offto the sets;Set.codRestrict f s h: givenh : ∀ x, f x ∈ s, restrict the codomain offto the sets;Set.MapsTo.restrict f s t h: givenh : MapsTo f s t, restrict the domain offtosand the codomain tot.
Restrict #
Restrict domain of a function f to a set s. Same as Subtype.restrict but this version
takes an argument ↥s instead of Subtype s.
Equations
- s.restrict f x = f ↑x
Instances For
theorem
Set.restrict_extend_range
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(g : α → γ)
(g' : β → γ)
:
(Set.range f).restrict (Function.extend f g g') = fun (x : ↑(Set.range f)) => g (Exists.choose ⋯)
@[simp]
theorem
Set.restrict_extend_compl_range
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(g : α → γ)
(g' : β → γ)
:
(Set.range f)ᶜ.restrict (Function.extend f g g') = g' ∘ Subtype.val
theorem
Set.range_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
(hf : Function.Injective f)
(g : α → γ)
(g' : β → γ)
:
def
Set.codRestrict
{α : Type u_1}
{ι : Sort u_4}
(f : ι → α)
(s : Set α)
(h : ∀ (x : ι), f x ∈ s)
:
ι → ↑s
Restrict codomain of a function f to a set s. Same as Subtype.coind but this version
has codomain ↥s instead of Subtype s.
Equations
- Set.codRestrict f s h x = ⟨f x, ⋯⟩
Instances For
@[simp]
theorem
Set.val_codRestrict_apply
{α : Type u_1}
{ι : Sort u_4}
(f : ι → α)
(s : Set α)
(h : ∀ (x : ι), f x ∈ s)
(x : ι)
:
↑(Set.codRestrict f s h x) = f x
@[simp]
theorem
Set.injective_codRestrict
{α : Type u_1}
{ι : Sort u_4}
{f : ι → α}
{s : Set α}
(h : ∀ (x : ι), f x ∈ s)
:
Function.Injective (Set.codRestrict f s h) ↔ Function.Injective f
theorem
Function.Injective.codRestrict
{α : Type u_1}
{ι : Sort u_4}
{f : ι → α}
{s : Set α}
(h : ∀ (x : ι), f x ∈ s)
:
Function.Injective f → Function.Injective (Set.codRestrict f s h)
Alias of the reverse direction of Set.injective_codRestrict.
Equality on a set #
Variant of EqOn.image_eq, for one function being the identity.
Congruence lemmas for monotonicity and antitonicity #
theorem
MonotoneOn.congr
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f₁ : α → β}
{f₂ : α → β}
[Preorder α]
[Preorder β]
(h₁ : MonotoneOn f₁ s)
(h : Set.EqOn f₁ f₂ s)
:
MonotoneOn f₂ s
theorem
AntitoneOn.congr
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f₁ : α → β}
{f₂ : α → β}
[Preorder α]
[Preorder β]
(h₁ : AntitoneOn f₁ s)
(h : Set.EqOn f₁ f₂ s)
:
AntitoneOn f₂ s
theorem
StrictMonoOn.congr
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f₁ : α → β}
{f₂ : α → β}
[Preorder α]
[Preorder β]
(h₁ : StrictMonoOn f₁ s)
(h : Set.EqOn f₁ f₂ s)
:
StrictMonoOn f₂ s
theorem
StrictAntiOn.congr
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f₁ : α → β}
{f₂ : α → β}
[Preorder α]
[Preorder β]
(h₁ : StrictAntiOn f₁ s)
(h : Set.EqOn f₁ f₂ s)
:
StrictAntiOn f₂ s
theorem
Set.EqOn.congr_monotoneOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f₁ : α → β}
{f₂ : α → β}
[Preorder α]
[Preorder β]
(h : Set.EqOn f₁ f₂ s)
:
MonotoneOn f₁ s ↔ MonotoneOn f₂ s
theorem
Set.EqOn.congr_antitoneOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f₁ : α → β}
{f₂ : α → β}
[Preorder α]
[Preorder β]
(h : Set.EqOn f₁ f₂ s)
:
AntitoneOn f₁ s ↔ AntitoneOn f₂ s
theorem
Set.EqOn.congr_strictMonoOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f₁ : α → β}
{f₂ : α → β}
[Preorder α]
[Preorder β]
(h : Set.EqOn f₁ f₂ s)
:
StrictMonoOn f₁ s ↔ StrictMonoOn f₂ s
theorem
Set.EqOn.congr_strictAntiOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f₁ : α → β}
{f₂ : α → β}
[Preorder α]
[Preorder β]
(h : Set.EqOn f₁ f₂ s)
:
StrictAntiOn f₁ s ↔ StrictAntiOn f₂ s
Monotonicity lemmas #
theorem
MonotoneOn.mono
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{s₂ : Set α}
{f : α → β}
[Preorder α]
[Preorder β]
(h : MonotoneOn f s)
(h' : s₂ ⊆ s)
:
MonotoneOn f s₂
theorem
AntitoneOn.mono
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{s₂ : Set α}
{f : α → β}
[Preorder α]
[Preorder β]
(h : AntitoneOn f s)
(h' : s₂ ⊆ s)
:
AntitoneOn f s₂
theorem
StrictMonoOn.mono
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{s₂ : Set α}
{f : α → β}
[Preorder α]
[Preorder β]
(h : StrictMonoOn f s)
(h' : s₂ ⊆ s)
:
StrictMonoOn f s₂
theorem
StrictAntiOn.mono
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{s₂ : Set α}
{f : α → β}
[Preorder α]
[Preorder β]
(h : StrictAntiOn f s)
(h' : s₂ ⊆ s)
:
StrictAntiOn f s₂
theorem
MonotoneOn.monotone
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
[Preorder α]
[Preorder β]
(h : MonotoneOn f s)
:
theorem
AntitoneOn.monotone
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
[Preorder α]
[Preorder β]
(h : AntitoneOn f s)
:
theorem
StrictMonoOn.strictMono
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
[Preorder α]
[Preorder β]
(h : StrictMonoOn f s)
:
StrictMono (f ∘ Subtype.val)
theorem
StrictAntiOn.strictAnti
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
[Preorder α]
[Preorder β]
(h : StrictAntiOn f s)
:
StrictAnti (f ∘ Subtype.val)
theorem
Set.MapsTo.restrict_commutes
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set α)
(t : Set β)
(h : Set.MapsTo f s t)
:
Subtype.val ∘ Set.MapsTo.restrict f s t h = f ∘ Subtype.val
@[simp]
theorem
Set.MapsTo.val_restrict_apply
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.MapsTo f s t)
(x : ↑s)
:
↑(Set.MapsTo.restrict f s t h x) = f ↑x
theorem
Set.MapsTo.coe_iterate_restrict
{α : Type u_1}
{s : Set α}
{f : α → α}
(h : Set.MapsTo f s s)
(x : ↑s)
(k : ℕ)
:
@[simp]
theorem
Set.codRestrict_restrict
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : ∀ (x : ↑s), f ↑x ∈ t)
:
Set.codRestrict (s.restrict f) t h = Set.MapsTo.restrict f s t ⋯
Restricting the domain and then the codomain is the same as MapsTo.restrict.
theorem
Set.MapsTo.restrict_eq_codRestrict
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.MapsTo f s t)
:
Set.MapsTo.restrict f s t h = Set.codRestrict (s.restrict f) t ⋯
Reverse of Set.codRestrict_restrict.
theorem
Set.MapsTo.coe_restrict
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.MapsTo f s t)
:
Subtype.val ∘ Set.MapsTo.restrict f s t h = s.restrict f
theorem
Set.MapsTo.range_restrict
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set α)
(t : Set β)
(h : Set.MapsTo f s t)
:
Set.range (Set.MapsTo.restrict f s t h) = Subtype.val ⁻¹' (f '' s)
theorem
Set.mapsTo_iff_exists_map_subtype
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
:
Set.MapsTo f s t ↔ ∃ (g : ↑s → ↑t), ∀ (x : ↑s), f ↑x = ↑(g x)
theorem
Set.mapsTo'
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
:
Set.MapsTo f s t ↔ f '' s ⊆ t
theorem
Set.mapsTo_prod_map_diagonal
{α : Type u_1}
{β : Type u_2}
{f : α → β}
:
Set.MapsTo (Prod.map f f) (Set.diagonal α) (Set.diagonal β)
theorem
Set.MapsTo.subset_preimage
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{s : Set α}
{t : Set β}
(hf : Set.MapsTo f s t)
:
@[simp]
theorem
Set.mapsTo_singleton
{α : Type u_1}
{β : Type u_2}
{t : Set β}
{f : α → β}
{x : α}
:
Set.MapsTo f {x} t ↔ f x ∈ t
@[simp]
theorem
Set.mapsTo_empty_iff
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
:
Set.MapsTo f s ∅ ↔ s = ∅
theorem
Set.MapsTo.nonempty
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.MapsTo f s t)
(hs : s.Nonempty)
:
t.Nonempty
If f maps s to t and s is non-empty, t is non-empty.
theorem
Set.MapsTo.image_subset
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.MapsTo f s t)
:
theorem
Set.MapsTo.congr
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f₁ : α → β}
{f₂ : α → β}
(h₁ : Set.MapsTo f₁ s t)
(h : Set.EqOn f₁ f₂ s)
:
Set.MapsTo f₂ s t
theorem
Set.EqOn.mapsTo_iff
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f₁ : α → β}
{f₂ : α → β}
(H : Set.EqOn f₁ f₂ s)
:
Set.MapsTo f₁ s t ↔ Set.MapsTo f₂ s t
theorem
Set.MapsTo.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{s : Set α}
{t : Set β}
{p : Set γ}
{f : α → β}
{g : β → γ}
(h₁ : Set.MapsTo g t p)
(h₂ : Set.MapsTo f s t)
:
Set.MapsTo (g ∘ f) s p
theorem
Set.MapsTo.iterate
{α : Type u_1}
{f : α → α}
{s : Set α}
(h : Set.MapsTo f s s)
(n : ℕ)
:
Set.MapsTo f^[n] s s
theorem
Set.MapsTo.iterate_restrict
{α : Type u_1}
{f : α → α}
{s : Set α}
(h : Set.MapsTo f s s)
(n : ℕ)
:
(Set.MapsTo.restrict f s s h)^[n] = Set.MapsTo.restrict f^[n] s s ⋯
theorem
Set.mapsTo_of_subsingleton'
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
[Subsingleton β]
(f : α → β)
(h : s.Nonempty → t.Nonempty)
:
Set.MapsTo f s t
theorem
Set.mapsTo_of_subsingleton
{α : Type u_1}
[Subsingleton α]
(f : α → α)
(s : Set α)
:
Set.MapsTo f s s
theorem
Set.MapsTo.mono
{α : Type u_1}
{β : Type u_2}
{s₁ : Set α}
{s₂ : Set α}
{t₁ : Set β}
{t₂ : Set β}
{f : α → β}
(hf : Set.MapsTo f s₁ t₁)
(hs : s₂ ⊆ s₁)
(ht : t₁ ⊆ t₂)
:
Set.MapsTo f s₂ t₂
theorem
Set.MapsTo.mono_left
{α : Type u_1}
{β : Type u_2}
{s₁ : Set α}
{s₂ : Set α}
{t : Set β}
{f : α → β}
(hf : Set.MapsTo f s₁ t)
(hs : s₂ ⊆ s₁)
:
Set.MapsTo f s₂ t
theorem
Set.MapsTo.mono_right
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t₁ : Set β}
{t₂ : Set β}
{f : α → β}
(hf : Set.MapsTo f s t₁)
(ht : t₁ ⊆ t₂)
:
Set.MapsTo f s t₂
theorem
Set.MapsTo.union_union
{α : Type u_1}
{β : Type u_2}
{s₁ : Set α}
{s₂ : Set α}
{t₁ : Set β}
{t₂ : Set β}
{f : α → β}
(h₁ : Set.MapsTo f s₁ t₁)
(h₂ : Set.MapsTo f s₂ t₂)
:
Set.MapsTo f (s₁ ∪ s₂) (t₁ ∪ t₂)
theorem
Set.MapsTo.union
{α : Type u_1}
{β : Type u_2}
{s₁ : Set α}
{s₂ : Set α}
{t : Set β}
{f : α → β}
(h₁ : Set.MapsTo f s₁ t)
(h₂ : Set.MapsTo f s₂ t)
:
Set.MapsTo f (s₁ ∪ s₂) t
@[simp]
theorem
Set.mapsTo_union
{α : Type u_1}
{β : Type u_2}
{s₁ : Set α}
{s₂ : Set α}
{t : Set β}
{f : α → β}
:
Set.MapsTo f (s₁ ∪ s₂) t ↔ Set.MapsTo f s₁ t ∧ Set.MapsTo f s₂ t
theorem
Set.MapsTo.inter
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t₁ : Set β}
{t₂ : Set β}
{f : α → β}
(h₁ : Set.MapsTo f s t₁)
(h₂ : Set.MapsTo f s t₂)
:
Set.MapsTo f s (t₁ ∩ t₂)
theorem
Set.MapsTo.inter_inter
{α : Type u_1}
{β : Type u_2}
{s₁ : Set α}
{s₂ : Set α}
{t₁ : Set β}
{t₂ : Set β}
{f : α → β}
(h₁ : Set.MapsTo f s₁ t₁)
(h₂ : Set.MapsTo f s₂ t₂)
:
Set.MapsTo f (s₁ ∩ s₂) (t₁ ∩ t₂)
@[simp]
theorem
Set.mapsTo_inter
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t₁ : Set β}
{t₂ : Set β}
{f : α → β}
:
Set.MapsTo f s (t₁ ∩ t₂) ↔ Set.MapsTo f s t₁ ∧ Set.MapsTo f s t₂
theorem
Set.mapsTo_univ
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set α)
:
Set.MapsTo f s Set.univ
theorem
Set.mapsTo_range
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set α)
:
Set.MapsTo f s (Set.range f)
@[simp]
theorem
Set.mapsTo_image_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{g : γ → α}
{s : Set γ}
{t : Set β}
:
Set.MapsTo f (g '' s) t ↔ Set.MapsTo (f ∘ g) s t
@[deprecated]
theorem
Set.maps_image_to
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(g : γ → α)
(s : Set γ)
(t : Set β)
:
Set.MapsTo f (g '' s) t ↔ Set.MapsTo (f ∘ g) s t
theorem
Set.MapsTo.comp_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{s : Set α}
{t : Set β}
{f : α → β}
(g : β → γ)
(hf : Set.MapsTo f s t)
:
Set.MapsTo (g ∘ f) s (g '' t)
theorem
Set.MapsTo.comp_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{g : β → γ}
{s : Set β}
{t : Set γ}
(hg : Set.MapsTo g s t)
(f : α → β)
:
Set.MapsTo (g ∘ f) (f ⁻¹' s) t
@[simp]
theorem
Set.mapsTo_univ_iff
{α : Type u_1}
{β : Type u_2}
{t : Set β}
{f : α → β}
:
Set.MapsTo f Set.univ t ↔ ∀ (x : α), f x ∈ t
@[deprecated]
theorem
Set.maps_univ_to
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set β)
:
Set.MapsTo f Set.univ s ↔ ∀ (a : α), f a ∈ s
@[simp]
theorem
Set.mapsTo_range_iff
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{t : Set β}
{f : α → β}
{g : ι → α}
:
Set.MapsTo f (Set.range g) t ↔ ∀ (i : ι), f (g i) ∈ t
@[deprecated Set.mapsTo_range_iff]
theorem
Set.maps_range_to
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(g : γ → α)
(s : Set β)
:
Set.MapsTo f (Set.range g) s ↔ Set.MapsTo (f ∘ g) Set.univ s
theorem
Set.surjective_mapsTo_image_restrict
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set α)
:
Function.Surjective (Set.MapsTo.restrict f s (f '' s) ⋯)
theorem
Set.MapsTo.mem_iff
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.MapsTo f s t)
(hc : Set.MapsTo f sᶜ tᶜ)
{x : α}
:
Restriction onto preimage #
theorem
Set.restrictPreimage_injective
{α : Type u_1}
{β : Type u_2}
(t : Set β)
{f : α → β}
(hf : Function.Injective f)
:
Function.Injective (t.restrictPreimage f)
theorem
Set.restrictPreimage_surjective
{α : Type u_1}
{β : Type u_2}
(t : Set β)
{f : α → β}
(hf : Function.Surjective f)
:
Function.Surjective (t.restrictPreimage f)
theorem
Set.restrictPreimage_bijective
{α : Type u_1}
{β : Type u_2}
(t : Set β)
{f : α → β}
(hf : Function.Bijective f)
:
Function.Bijective (t.restrictPreimage f)
theorem
Function.Injective.restrictPreimage
{α : Type u_1}
{β : Type u_2}
(t : Set β)
{f : α → β}
(hf : Function.Injective f)
:
Function.Injective (t.restrictPreimage f)
Alias of Set.restrictPreimage_injective.
theorem
Function.Surjective.restrictPreimage
{α : Type u_1}
{β : Type u_2}
(t : Set β)
{f : α → β}
(hf : Function.Surjective f)
:
Function.Surjective (t.restrictPreimage f)
Alias of Set.restrictPreimage_surjective.
theorem
Function.Bijective.restrictPreimage
{α : Type u_1}
{β : Type u_2}
(t : Set β)
{f : α → β}
(hf : Function.Bijective f)
:
Function.Bijective (t.restrictPreimage f)
Alias of Set.restrictPreimage_bijective.
Injectivity on a set #
@[simp]
theorem
Set.injective_iff_injOn_univ
{α : Type u_1}
{β : Type u_2}
{f : α → β}
:
Function.Injective f ↔ Set.InjOn f Set.univ
theorem
Set.injOn_of_injective
{α : Type u_1}
{β : Type u_2}
{f : α → β}
(h : Function.Injective f)
{s : Set α}
:
Set.InjOn f s
theorem
Function.Injective.injOn
{α : Type u_1}
{β : Type u_2}
{f : α → β}
(h : Function.Injective f)
{s : Set α}
:
Set.InjOn f s
Alias of Set.injOn_of_injective.
theorem
Set.InjOn.iterate
{α : Type u_1}
{f : α → α}
{s : Set α}
(h : Set.InjOn f s)
(hf : Set.MapsTo f s s)
(n : ℕ)
:
theorem
Set.injOn_of_subsingleton
{α : Type u_1}
{β : Type u_2}
[Subsingleton α]
(f : α → β)
(s : Set α)
:
Set.InjOn f s
theorem
Function.Injective.injOn_range
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{g : β → γ}
(h : Function.Injective (g ∘ f))
:
theorem
Set.injOn_iff_injective
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
:
Set.InjOn f s ↔ Function.Injective (s.restrict f)
theorem
Set.InjOn.injective
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
:
Set.InjOn f s → Function.Injective (s.restrict f)
Alias of the forward direction of Set.injOn_iff_injective.
theorem
Set.MapsTo.restrict_inj
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.MapsTo f s t)
:
Function.Injective (Set.MapsTo.restrict f s t h) ↔ Set.InjOn f s
theorem
Set.exists_injOn_iff_injective
{α : Type u_1}
{β : Type u_2}
{s : Set α}
[Nonempty β]
:
(∃ (f : α → β), Set.InjOn f s) ↔ ∃ (f : ↑s → β), Function.Injective f
theorem
Set.EqOn.cancel_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{s : Set α}
{t : Set β}
{f₁ : α → β}
{f₂ : α → β}
{g : β → γ}
(h : Set.EqOn (g ∘ f₁) (g ∘ f₂) s)
(hg : Set.InjOn g t)
(hf₁ : Set.MapsTo f₁ s t)
(hf₂ : Set.MapsTo f₂ s t)
:
Set.EqOn f₁ f₂ s
theorem
Set.InjOn.cancel_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{s : Set α}
{t : Set β}
{f₁ : α → β}
{f₂ : α → β}
{g : β → γ}
(hg : Set.InjOn g t)
(hf₁ : Set.MapsTo f₁ s t)
(hf₂ : Set.MapsTo f₂ s t)
:
theorem
Set.InjOn.imageFactorization_injective
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
(h : Set.InjOn f s)
:
@[simp]
theorem
Set.imageFactorization_injective_iff
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
:
Function.Injective (Set.imageFactorization f s) ↔ Set.InjOn f s
@[simp]
@[simp]
theorem
Set.graphOn_union
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set α)
(t : Set α)
:
Set.graphOn f (s ∪ t) = Set.graphOn f s ∪ Set.graphOn f t
@[simp]
theorem
Set.graphOn_singleton
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(x : α)
:
Set.graphOn f {x} = {(x, f x)}
@[simp]
theorem
Set.graphOn_insert
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(x : α)
(s : Set α)
:
Set.graphOn f (insert x s) = insert (x, f x) (Set.graphOn f s)
@[simp]
theorem
Set.image_fst_graphOn
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set α)
:
Prod.fst '' Set.graphOn f s = s
Surjectivity on a set #
theorem
Set.SurjOn.subset_range
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.SurjOn f s t)
:
theorem
Set.surjOn_iff_exists_map_subtype
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
:
Set.SurjOn f s t ↔ ∃ (t' : Set β) (g : ↑s → ↑t'), t ⊆ t' ∧ Function.Surjective g ∧ ∀ (x : ↑s), f ↑x = ↑(g x)
@[simp]
theorem
Set.surjOn_empty_iff
{α : Type u_1}
{β : Type u_2}
{t : Set β}
{f : α → β}
:
Set.SurjOn f ∅ t ↔ t = ∅
@[simp]
theorem
Set.surjOn_singleton
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
{b : β}
:
Set.SurjOn f s {b} ↔ b ∈ f '' s
theorem
Set.surjOn_image
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set α)
:
Set.SurjOn f s (f '' s)
theorem
Set.SurjOn.comap_nonempty
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.SurjOn f s t)
(ht : t.Nonempty)
:
s.Nonempty
theorem
Set.SurjOn.congr
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f₁ : α → β}
{f₂ : α → β}
(h : Set.SurjOn f₁ s t)
(H : Set.EqOn f₁ f₂ s)
:
Set.SurjOn f₂ s t
theorem
Set.EqOn.surjOn_iff
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f₁ : α → β}
{f₂ : α → β}
(h : Set.EqOn f₁ f₂ s)
:
Set.SurjOn f₁ s t ↔ Set.SurjOn f₂ s t
theorem
Set.SurjOn.mono
{α : Type u_1}
{β : Type u_2}
{s₁ : Set α}
{s₂ : Set α}
{t₁ : Set β}
{t₂ : Set β}
{f : α → β}
(hs : s₁ ⊆ s₂)
(ht : t₁ ⊆ t₂)
(hf : Set.SurjOn f s₁ t₂)
:
Set.SurjOn f s₂ t₁
theorem
Set.SurjOn.union
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t₁ : Set β}
{t₂ : Set β}
{f : α → β}
(h₁ : Set.SurjOn f s t₁)
(h₂ : Set.SurjOn f s t₂)
:
Set.SurjOn f s (t₁ ∪ t₂)
theorem
Set.SurjOn.union_union
{α : Type u_1}
{β : Type u_2}
{s₁ : Set α}
{s₂ : Set α}
{t₁ : Set β}
{t₂ : Set β}
{f : α → β}
(h₁ : Set.SurjOn f s₁ t₁)
(h₂ : Set.SurjOn f s₂ t₂)
:
Set.SurjOn f (s₁ ∪ s₂) (t₁ ∪ t₂)
theorem
Set.SurjOn.inter_inter
{α : Type u_1}
{β : Type u_2}
{s₁ : Set α}
{s₂ : Set α}
{t₁ : Set β}
{t₂ : Set β}
{f : α → β}
(h₁ : Set.SurjOn f s₁ t₁)
(h₂ : Set.SurjOn f s₂ t₂)
(h : Set.InjOn f (s₁ ∪ s₂))
:
Set.SurjOn f (s₁ ∩ s₂) (t₁ ∩ t₂)
theorem
Set.SurjOn.inter
{α : Type u_1}
{β : Type u_2}
{s₁ : Set α}
{s₂ : Set α}
{t : Set β}
{f : α → β}
(h₁ : Set.SurjOn f s₁ t)
(h₂ : Set.SurjOn f s₂ t)
(h : Set.InjOn f (s₁ ∪ s₂))
:
Set.SurjOn f (s₁ ∩ s₂) t
theorem
Set.SurjOn.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{s : Set α}
{t : Set β}
{p : Set γ}
{f : α → β}
{g : β → γ}
(hg : Set.SurjOn g t p)
(hf : Set.SurjOn f s t)
:
Set.SurjOn (g ∘ f) s p
theorem
Set.SurjOn.iterate
{α : Type u_1}
{f : α → α}
{s : Set α}
(h : Set.SurjOn f s s)
(n : ℕ)
:
Set.SurjOn f^[n] s s
theorem
Set.SurjOn.comp_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{s : Set α}
{t : Set β}
{f : α → β}
(hf : Set.SurjOn f s t)
(g : β → γ)
:
Set.SurjOn (g ∘ f) s (g '' t)
theorem
Set.SurjOn.comp_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{g : β → γ}
{s : Set β}
{t : Set γ}
(hf : Function.Surjective f)
(hg : Set.SurjOn g s t)
:
Set.SurjOn (g ∘ f) (f ⁻¹' s) t
theorem
Set.surjOn_of_subsingleton'
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
[Subsingleton β]
(f : α → β)
(h : t.Nonempty → s.Nonempty)
:
Set.SurjOn f s t
theorem
Set.surjOn_of_subsingleton
{α : Type u_1}
[Subsingleton α]
(f : α → α)
(s : Set α)
:
Set.SurjOn f s s
theorem
Set.surjective_iff_surjOn_univ
{α : Type u_1}
{β : Type u_2}
{f : α → β}
:
Function.Surjective f ↔ Set.SurjOn f Set.univ Set.univ
theorem
Set.surjOn_iff_surjective
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
:
Set.SurjOn f s Set.univ ↔ Function.Surjective (s.restrict f)
@[simp]
theorem
Set.MapsTo.restrict_surjective_iff
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.MapsTo f s t)
:
Function.Surjective (Set.MapsTo.restrict f s t h) ↔ Set.SurjOn f s t
theorem
Set.SurjOn.image_eq_of_mapsTo
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h₁ : Set.SurjOn f s t)
(h₂ : Set.MapsTo f s t)
:
theorem
Set.image_eq_iff_surjOn_mapsTo
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
:
f '' s = t ↔ Set.SurjOn f s t ∧ Set.MapsTo f s t
theorem
Set.SurjOn.mapsTo_compl
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.SurjOn f s t)
(h' : Function.Injective f)
:
Set.MapsTo f sᶜ tᶜ
theorem
Set.MapsTo.surjOn_compl
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.MapsTo f s t)
(h' : Function.Surjective f)
:
Set.SurjOn f sᶜ tᶜ
theorem
Set.SurjOn.cancel_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{s : Set α}
{t : Set β}
{f : α → β}
{g₁ : β → γ}
{g₂ : β → γ}
(hf : Set.SurjOn f s t)
(hf' : Set.MapsTo f s t)
:
theorem
Set.SurjOn.forall
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
{p : β → Prop}
(hf : Set.SurjOn f s t)
(hf' : Set.MapsTo f s t)
:
(∀ y ∈ t, p y) ↔ ∀ x ∈ s, p (f x)
Bijectivity #
theorem
Set.BijOn.mapsTo
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.BijOn f s t)
:
Set.MapsTo f s t
theorem
Set.BijOn.surjOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.BijOn f s t)
:
Set.SurjOn f s t
theorem
Set.BijOn.mk
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h₁ : Set.MapsTo f s t)
(h₂ : Set.InjOn f s)
(h₃ : Set.SurjOn f s t)
:
Set.BijOn f s t
theorem
Set.bijOn_of_subsingleton'
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
[Subsingleton α]
[Subsingleton β]
(f : α → β)
(h : s.Nonempty ↔ t.Nonempty)
:
Set.BijOn f s t
theorem
Set.bijOn_of_subsingleton
{α : Type u_1}
[Subsingleton α]
(f : α → α)
(s : Set α)
:
Set.BijOn f s s
theorem
Set.BijOn.bijective
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.BijOn f s t)
:
Function.Bijective (Set.MapsTo.restrict f s t ⋯)
theorem
Set.bijective_iff_bijOn_univ
{α : Type u_1}
{β : Type u_2}
{f : α → β}
:
Function.Bijective f ↔ Set.BijOn f Set.univ Set.univ
theorem
Function.Bijective.bijOn_univ
{α : Type u_1}
{β : Type u_2}
{f : α → β}
:
Function.Bijective f → Set.BijOn f Set.univ Set.univ
Alias of the forward direction of Set.bijective_iff_bijOn_univ.
left inverse #
theorem
Set.LeftInvOn.eqOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
{f' : β → α}
(h : Set.LeftInvOn f' f s)
:
theorem
Set.LeftInvOn.eq
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
{f' : β → α}
(h : Set.LeftInvOn f' f s)
{x : α}
(hx : x ∈ s)
:
f' (f x) = x
theorem
Set.LeftInvOn.congr_left
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
{f₁' : β → α}
{f₂' : β → α}
(h₁ : Set.LeftInvOn f₁' f s)
{t : Set β}
(h₁' : Set.MapsTo f s t)
(heq : Set.EqOn f₁' f₂' t)
:
Set.LeftInvOn f₂' f s
theorem
Set.LeftInvOn.congr_right
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f₁ : α → β}
{f₂ : α → β}
{f₁' : β → α}
(h₁ : Set.LeftInvOn f₁' f₁ s)
(heq : Set.EqOn f₁ f₂ s)
:
Set.LeftInvOn f₁' f₂ s
theorem
Set.LeftInvOn.injOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
{f₁' : β → α}
(h : Set.LeftInvOn f₁' f s)
:
Set.InjOn f s
theorem
Set.LeftInvOn.surjOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
{f' : β → α}
(h : Set.LeftInvOn f' f s)
(hf : Set.MapsTo f s t)
:
Set.SurjOn f' t s
theorem
Set.LeftInvOn.mapsTo
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
{f' : β → α}
(h : Set.LeftInvOn f' f s)
(hf : Set.SurjOn f s t)
:
Set.MapsTo f' t s
theorem
Set.LeftInvOn.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{s : Set α}
{t : Set β}
{f : α → β}
{g : β → γ}
{f' : β → α}
{g' : γ → β}
(hf' : Set.LeftInvOn f' f s)
(hg' : Set.LeftInvOn g' g t)
(hf : Set.MapsTo f s t)
:
Set.LeftInvOn (f' ∘ g') (g ∘ f) s
theorem
Set.LeftInvOn.mono
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{s₁ : Set α}
{f : α → β}
{f' : β → α}
(hf : Set.LeftInvOn f' f s)
(ht : s₁ ⊆ s)
:
Set.LeftInvOn f' f s₁
theorem
Set.LeftInvOn.image_image
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
{f' : β → α}
(hf : Set.LeftInvOn f' f s)
:
Right inverse #
theorem
Set.RightInvOn.eqOn
{α : Type u_1}
{β : Type u_2}
{t : Set β}
{f : α → β}
{f' : β → α}
(h : Set.RightInvOn f' f t)
:
theorem
Set.RightInvOn.eq
{α : Type u_1}
{β : Type u_2}
{t : Set β}
{f : α → β}
{f' : β → α}
(h : Set.RightInvOn f' f t)
{y : β}
(hy : y ∈ t)
:
f (f' y) = y
theorem
Set.LeftInvOn.rightInvOn_image
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
{f' : β → α}
(h : Set.LeftInvOn f' f s)
:
Set.RightInvOn f' f (f '' s)
theorem
Set.RightInvOn.congr_left
{α : Type u_1}
{β : Type u_2}
{t : Set β}
{f : α → β}
{f₁' : β → α}
{f₂' : β → α}
(h₁ : Set.RightInvOn f₁' f t)
(heq : Set.EqOn f₁' f₂' t)
:
Set.RightInvOn f₂' f t
theorem
Set.RightInvOn.congr_right
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f₁ : α → β}
{f₂ : α → β}
{f' : β → α}
(h₁ : Set.RightInvOn f' f₁ t)
(hg : Set.MapsTo f' t s)
(heq : Set.EqOn f₁ f₂ s)
:
Set.RightInvOn f' f₂ t
theorem
Set.RightInvOn.surjOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
{f' : β → α}
(hf : Set.RightInvOn f' f t)
(hf' : Set.MapsTo f' t s)
:
Set.SurjOn f s t
theorem
Set.RightInvOn.mapsTo
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
{f' : β → α}
(h : Set.RightInvOn f' f t)
(hf : Set.SurjOn f' t s)
:
Set.MapsTo f s t
theorem
Set.RightInvOn.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{t : Set β}
{p : Set γ}
{f : α → β}
{g : β → γ}
{f' : β → α}
{g' : γ → β}
(hf : Set.RightInvOn f' f t)
(hg : Set.RightInvOn g' g p)
(g'pt : Set.MapsTo g' p t)
:
Set.RightInvOn (f' ∘ g') (g ∘ f) p
theorem
Set.RightInvOn.mono
{α : Type u_1}
{β : Type u_2}
{t : Set β}
{t₁ : Set β}
{f : α → β}
{f' : β → α}
(hf : Set.RightInvOn f' f t)
(ht : t₁ ⊆ t)
:
Set.RightInvOn f' f t₁
theorem
Set.InjOn.rightInvOn_of_leftInvOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
{f' : β → α}
(hf : Set.InjOn f s)
(hf' : Set.LeftInvOn f f' t)
(h₁ : Set.MapsTo f s t)
(h₂ : Set.MapsTo f' t s)
:
Set.RightInvOn f f' s
theorem
Set.eqOn_of_leftInvOn_of_rightInvOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
{f₁' : β → α}
{f₂' : β → α}
(h₁ : Set.LeftInvOn f₁' f s)
(h₂ : Set.RightInvOn f₂' f t)
(h : Set.MapsTo f₂' t s)
:
Set.EqOn f₁' f₂' t
theorem
Set.SurjOn.leftInvOn_of_rightInvOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
{f' : β → α}
(hf : Set.SurjOn f s t)
(hf' : Set.RightInvOn f f' s)
:
Set.LeftInvOn f f' t
Two-side inverses #
theorem
Set.InvOn.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{s : Set α}
{t : Set β}
{p : Set γ}
{f : α → β}
{g : β → γ}
{f' : β → α}
{g' : γ → β}
(hf : Set.InvOn f' f s t)
(hg : Set.InvOn g' g t p)
(fst : Set.MapsTo f s t)
(g'pt : Set.MapsTo g' p t)
:
theorem
Set.InvOn.bijOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
{f' : β → α}
(h : Set.InvOn f' f s t)
(hf : Set.MapsTo f s t)
(hf' : Set.MapsTo f' t s)
:
Set.BijOn f s t
If functions f' and f are inverse on s and t, f maps s into t, and f' maps t
into s, then f is a bijection between s and t. The mapsTo arguments can be deduced from
surjOn statements using LeftInvOn.mapsTo and RightInvOn.mapsTo.
noncomputable def
Function.invFunOn
{α : Type u_1}
{β : Type u_2}
[Nonempty α]
(f : α → β)
(s : Set α)
(b : β)
:
α
Construct the inverse for a function f on domain s. This function is a right inverse of f
on f '' s. For a computable version, see Function.Embedding.invOfMemRange.
Equations
- Function.invFunOn f s b = if h : ∃ a ∈ s, f a = b then Classical.choose h else Classical.choice inst
Instances For
theorem
Function.invFunOn_pos
{α : Type u_1}
{β : Type u_2}
[Nonempty α]
{s : Set α}
{f : α → β}
{b : β}
(h : ∃ a ∈ s, f a = b)
:
Function.invFunOn f s b ∈ s ∧ f (Function.invFunOn f s b) = b
theorem
Function.invFunOn_mem
{α : Type u_1}
{β : Type u_2}
[Nonempty α]
{s : Set α}
{f : α → β}
{b : β}
(h : ∃ a ∈ s, f a = b)
:
Function.invFunOn f s b ∈ s
theorem
Function.invFunOn_eq
{α : Type u_1}
{β : Type u_2}
[Nonempty α]
{s : Set α}
{f : α → β}
{b : β}
(h : ∃ a ∈ s, f a = b)
:
f (Function.invFunOn f s b) = b
theorem
Function.invFunOn_neg
{α : Type u_1}
{β : Type u_2}
[Nonempty α]
{s : Set α}
{f : α → β}
{b : β}
(h : ¬∃ a ∈ s, f a = b)
:
Function.invFunOn f s b = Classical.choice inst✝
@[simp]
theorem
Function.invFunOn_apply_mem
{α : Type u_1}
{β : Type u_2}
[Nonempty α]
{s : Set α}
{f : α → β}
{a : α}
(h : a ∈ s)
:
Function.invFunOn f s (f a) ∈ s
theorem
Function.invFunOn_apply_eq
{α : Type u_1}
{β : Type u_2}
[Nonempty α]
{s : Set α}
{f : α → β}
{a : α}
(h : a ∈ s)
:
f (Function.invFunOn f s (f a)) = f a
theorem
Set.InjOn.leftInvOn_invFunOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
[Nonempty α]
(h : Set.InjOn f s)
:
Set.LeftInvOn (Function.invFunOn f s) f s
theorem
Function.leftInvOn_invFunOn_of_subset_image_image
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
[Nonempty α]
(h : s ⊆ Function.invFunOn f s '' (f '' s))
:
Set.LeftInvOn (Function.invFunOn f s) f s
theorem
Function.invFunOn_injOn_image
{α : Type u_1}
{β : Type u_2}
[Nonempty α]
(f : α → β)
(s : Set α)
:
Set.InjOn (Function.invFunOn f s) (f '' s)
theorem
Function.invFunOn_image_image_subset
{α : Type u_1}
{β : Type u_2}
[Nonempty α]
(f : α → β)
(s : Set α)
:
Function.invFunOn f s '' (f '' s) ⊆ s
theorem
Set.SurjOn.rightInvOn_invFunOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
[Nonempty α]
(h : Set.SurjOn f s t)
:
Set.RightInvOn (Function.invFunOn f s) f t
theorem
Set.BijOn.invOn_invFunOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
[Nonempty α]
(h : Set.BijOn f s t)
:
Set.InvOn (Function.invFunOn f s) f s t
theorem
Set.SurjOn.invOn_invFunOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
[Nonempty α]
(h : Set.SurjOn f s t)
:
Set.InvOn (Function.invFunOn f s) f (Function.invFunOn f s '' t) t
theorem
Set.SurjOn.mapsTo_invFunOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
[Nonempty α]
(h : Set.SurjOn f s t)
:
Set.MapsTo (Function.invFunOn f s) t s
theorem
Set.SurjOn.image_invFunOn_image_of_subset
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
[Nonempty α]
{r : Set β}
(hf : Set.SurjOn f s t)
(hrt : r ⊆ t)
:
f '' (Function.invFunOn f s '' r) = r
This lemma is a special case of rightInvOn_invFunOn.image_image'; it may make more sense
to use the other lemma directly in an application.
theorem
Set.SurjOn.image_invFunOn_image
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
[Nonempty α]
(hf : Set.SurjOn f s t)
:
f '' (Function.invFunOn f s '' t) = t
This lemma is a special case of rightInvOn_invFunOn.image_image; it may make more sense
to use the other lemma directly in an application.
theorem
Set.SurjOn.bijOn_subset
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
[Nonempty α]
(h : Set.SurjOn f s t)
:
Set.BijOn f (Function.invFunOn f s '' t) t
theorem
Set.surjOn_iff_exists_bijOn_subset
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
:
Set.SurjOn f s t ↔ ∃ s' ⊆ s, Set.BijOn f s' t
theorem
Set.SurjOn.exists_bijOn_subset
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
:
Set.SurjOn f s t → ∃ s' ⊆ s, Set.BijOn f s' t
Alias of the forward direction of Set.surjOn_iff_exists_bijOn_subset.
theorem
Set.BijOn.exists_extend_of_subset
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{s₁ : Set α}
{t : Set β}
{f : α → β}
{t' : Set β}
(h : Set.BijOn f s t)
(hss₁ : s ⊆ s₁)
(htt' : t ⊆ t')
(ht' : Set.SurjOn f s₁ t')
:
If f maps s bijectively to t and a set t' is contained in the image of some s₁ ⊇ s,
then s₁ has a subset containing s that f maps bijectively to t'.
theorem
Set.BijOn.exists_extend
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
{t' : Set β}
(h : Set.BijOn f s t)
(htt' : t ⊆ t')
(ht' : t' ⊆ Set.range f)
:
If f maps s bijectively to t, and t' is a superset of t contained in the range of f,
then f maps some superset of s bijectively to t'.
theorem
Set.preimage_invFun_of_mem
{α : Type u_1}
{β : Type u_2}
[n : Nonempty α]
{f : α → β}
(hf : Function.Injective f)
{s : Set α}
(h : Classical.choice n ∈ s)
:
theorem
Set.preimage_invFun_of_not_mem
{α : Type u_1}
{β : Type u_2}
[n : Nonempty α]
{f : α → β}
(hf : Function.Injective f)
{s : Set α}
(h : Classical.choice n ∉ s)
:
Function.invFun f ⁻¹' s = f '' s
Monotone #
Piecewise defined function #
theorem
Set.piecewise_insert
{α : Type u_1}
{δ : α → Sort u_6}
(s : Set α)
(f : (i : α) → δ i)
(g : (i : α) → δ i)
[(j : α) → Decidable (j ∈ s)]
[DecidableEq α]
(j : α)
[(i : α) → Decidable (i ∈ insert j s)]
:
(insert j s).piecewise f g = Function.update (s.piecewise f g) j (f j)
theorem
Set.piecewise_singleton
{α : Type u_1}
{β : Type u_2}
(x : α)
[(y : α) → Decidable (y ∈ {x})]
[DecidableEq α]
(f : α → β)
(g : α → β)
:
{x}.piecewise f g = Function.update g x (f x)
theorem
Set.piecewise_le_piecewise
{α : Type u_1}
{δ : α → Type u_7}
[(i : α) → Preorder (δ i)]
{s : Set α}
[(j : α) → Decidable (j ∈ s)]
{f₁ : (i : α) → δ i}
{f₂ : (i : α) → δ i}
{g₁ : (i : α) → δ i}
{g₂ : (i : α) → δ i}
(h₁ : ∀ i ∈ s, f₁ i ≤ g₁ i)
(h₂ : ∀ i ∉ s, f₂ i ≤ g₂ i)
:
s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂
theorem
Set.MapsTo.piecewise_ite
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{s₁ : Set α}
{s₂ : Set α}
{t : Set β}
{t₁ : Set β}
{t₂ : Set β}
{f₁ : α → β}
{f₂ : α → β}
[(i : α) → Decidable (i ∈ s)]
(h₁ : Set.MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t))
(h₂ : Set.MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ))
:
Set.MapsTo (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)
theorem
Set.apply_piecewise₂
{α : Type u_1}
{δ : α → Sort u_6}
(s : Set α)
(f : (i : α) → δ i)
(g : (i : α) → δ i)
[(j : α) → Decidable (j ∈ s)]
{δ' : α → Sort u_7}
{δ'' : α → Sort u_8}
(f' : (i : α) → δ' i)
(g' : (i : α) → δ' i)
(h : (i : α) → δ i → δ' i → δ'' i)
{x : α}
:
h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun (x : α) => h x (f x) (f' x)) (fun (x : α) => h x (g x) (g' x)) x
theorem
Set.piecewise_op₂
{α : Type u_1}
{δ : α → Sort u_6}
(s : Set α)
(f : (i : α) → δ i)
(g : (i : α) → δ i)
[(j : α) → Decidable (j ∈ s)]
{δ' : α → Sort u_7}
{δ'' : α → Sort u_8}
(f' : (i : α) → δ' i)
(g' : (i : α) → δ' i)
(h : (i : α) → δ i → δ' i → δ'' i)
:
(s.piecewise (fun (x : α) => h x (f x) (f' x)) fun (x : α) => h x (g x) (g' x)) = fun (x : α) =>
h x (s.piecewise f g x) (s.piecewise f' g' x)
theorem
StrictMonoOn.injOn
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[Preorder β]
{f : α → β}
{s : Set α}
(H : StrictMonoOn f s)
:
Set.InjOn f s
theorem
StrictAntiOn.injOn
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[Preorder β]
{f : α → β}
{s : Set α}
(H : StrictAntiOn f s)
:
Set.InjOn f s
theorem
StrictMonoOn.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
[Preorder γ]
{g : β → γ}
{f : α → β}
{s : Set α}
{t : Set β}
(hg : StrictMonoOn g t)
(hf : StrictMonoOn f s)
(hs : Set.MapsTo f s t)
:
StrictMonoOn (g ∘ f) s
theorem
StrictMonoOn.comp_strictAntiOn
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
[Preorder γ]
{g : β → γ}
{f : α → β}
{s : Set α}
{t : Set β}
(hg : StrictMonoOn g t)
(hf : StrictAntiOn f s)
(hs : Set.MapsTo f s t)
:
StrictAntiOn (g ∘ f) s
theorem
StrictAntiOn.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
[Preorder γ]
{g : β → γ}
{f : α → β}
{s : Set α}
{t : Set β}
(hg : StrictAntiOn g t)
(hf : StrictAntiOn f s)
(hs : Set.MapsTo f s t)
:
StrictMonoOn (g ∘ f) s
theorem
StrictAntiOn.comp_strictMonoOn
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
[Preorder γ]
{g : β → γ}
{f : α → β}
{s : Set α}
{t : Set β}
(hg : StrictAntiOn g t)
(hf : StrictMonoOn f s)
(hs : Set.MapsTo f s t)
:
StrictAntiOn (g ∘ f) s
@[simp]
theorem
strictMono_restrict
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{f : α → β}
{s : Set α}
:
StrictMono (s.restrict f) ↔ StrictMonoOn f s
theorem
StrictMonoOn.restrict
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{f : α → β}
{s : Set α}
:
StrictMonoOn f s → StrictMono (s.restrict f)
Alias of the reverse direction of strictMono_restrict.
theorem
StrictMono.of_restrict
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{f : α → β}
{s : Set α}
:
StrictMono (s.restrict f) → StrictMonoOn f s
Alias of the forward direction of strictMono_restrict.
theorem
StrictMono.codRestrict
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{f : α → β}
(hf : StrictMono f)
{s : Set β}
(hs : ∀ (x : α), f x ∈ s)
:
StrictMono (Set.codRestrict f s hs)
theorem
Function.Injective.comp_injOn
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{g : β → γ}
{s : Set α}
(hg : Function.Injective g)
(hf : Set.InjOn f s)
:
theorem
Function.Surjective.surjOn
{α : Type u_1}
{β : Type u_2}
{f : α → β}
(hf : Function.Surjective f)
(s : Set β)
:
Set.SurjOn f Set.univ s
theorem
Function.LeftInverse.leftInvOn
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{g : β → α}
(h : Function.LeftInverse f g)
(s : Set β)
:
Set.LeftInvOn f g s
theorem
Function.RightInverse.rightInvOn
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{g : β → α}
(h : Function.RightInverse f g)
(s : Set α)
:
Set.RightInvOn f g s
theorem
Function.LeftInverse.rightInvOn_range
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{g : β → α}
(h : Function.LeftInverse f g)
:
Set.RightInvOn f g (Set.range g)
theorem
Function.Semiconj.mapsTo_image
{α : Type u_1}
{β : Type u_2}
{fa : α → α}
{fb : β → β}
{f : α → β}
{s : Set α}
{t : Set α}
(h : Function.Semiconj f fa fb)
(ha : Set.MapsTo fa s t)
:
Set.MapsTo fb (f '' s) (f '' t)
theorem
Function.Semiconj.mapsTo_range
{α : Type u_1}
{β : Type u_2}
{fa : α → α}
{fb : β → β}
{f : α → β}
(h : Function.Semiconj f fa fb)
:
Set.MapsTo fb (Set.range f) (Set.range f)
theorem
Function.Semiconj.surjOn_image
{α : Type u_1}
{β : Type u_2}
{fa : α → α}
{fb : β → β}
{f : α → β}
{s : Set α}
{t : Set α}
(h : Function.Semiconj f fa fb)
(ha : Set.SurjOn fa s t)
:
Set.SurjOn fb (f '' s) (f '' t)
theorem
Function.Semiconj.surjOn_range
{α : Type u_1}
{β : Type u_2}
{fa : α → α}
{fb : β → β}
{f : α → β}
(h : Function.Semiconj f fa fb)
(ha : Function.Surjective fa)
:
Set.SurjOn fb (Set.range f) (Set.range f)
theorem
Function.Semiconj.injOn_range
{α : Type u_1}
{β : Type u_2}
{fa : α → α}
{fb : β → β}
{f : α → β}
(h : Function.Semiconj f fa fb)
(ha : Function.Injective fa)
(hf : Set.InjOn f (Set.range fa))
:
theorem
Function.Semiconj.bijOn_range
{α : Type u_1}
{β : Type u_2}
{fa : α → α}
{fb : β → β}
{f : α → β}
(h : Function.Semiconj f fa fb)
(ha : Function.Bijective fa)
(hf : Function.Injective f)
:
theorem
Function.Semiconj.mapsTo_preimage
{α : Type u_1}
{β : Type u_2}
{fa : α → α}
{fb : β → β}
{f : α → β}
(h : Function.Semiconj f fa fb)
{s : Set β}
{t : Set β}
(hb : Set.MapsTo fb s t)
:
Set.MapsTo fa (f ⁻¹' s) (f ⁻¹' t)
theorem
Function.update_comp_eq_of_not_mem_range'
{α : Sort u_6}
{β : Type u_7}
{γ : β → Sort u_8}
[DecidableEq β]
(g : (b : β) → γ b)
{f : α → β}
{i : β}
(a : γ i)
(h : i ∉ Set.range f)
:
(fun (j : α) => Function.update g i a (f j)) = fun (j : α) => g (f j)
theorem
Function.update_comp_eq_of_not_mem_range
{α : Sort u_6}
{β : Type u_7}
{γ : Sort u_8}
[DecidableEq β]
(g : β → γ)
{f : α → β}
{i : β}
(a : γ)
(h : i ∉ Set.range f)
:
Function.update g i a ∘ f = g ∘ f
Non-dependent version of Function.update_comp_eq_of_not_mem_range'
theorem
Function.monotoneOn_of_rightInvOn_of_mapsTo
{α : Type u_6}
{β : Type u_7}
[PartialOrder α]
[LinearOrder β]
{φ : β → α}
{ψ : α → β}
{t : Set β}
{s : Set α}
(hφ : MonotoneOn φ t)
(φψs : Set.RightInvOn ψ φ s)
(ψts : Set.MapsTo ψ s t)
:
MonotoneOn ψ s
theorem
Function.antitoneOn_of_rightInvOn_of_mapsTo
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[LinearOrder β]
{φ : β → α}
{ψ : α → β}
{t : Set β}
{s : Set α}
(hφ : AntitoneOn φ t)
(φψs : Set.RightInvOn ψ φ s)
(ψts : Set.MapsTo ψ s t)
:
AntitoneOn ψ s
Equivalences, permutations #
theorem
Set.MapsTo.extendDomain
{α : Type u_1}
{β : Type u_2}
{p : β → Prop}
[DecidablePred p]
{f : α ≃ Subtype p}
{g : Equiv.Perm α}
{s : Set α}
{t : Set α}
(h : Set.MapsTo (⇑g) s t)
:
Set.MapsTo (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)
theorem
Set.SurjOn.extendDomain
{α : Type u_1}
{β : Type u_2}
{p : β → Prop}
[DecidablePred p]
{f : α ≃ Subtype p}
{g : Equiv.Perm α}
{s : Set α}
{t : Set α}
(h : Set.SurjOn (⇑g) s t)
:
Set.SurjOn (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)
theorem
Set.LeftInvOn.extendDomain
{α : Type u_1}
{β : Type u_2}
{p : β → Prop}
[DecidablePred p]
{f : α ≃ Subtype p}
{g₁ : Equiv.Perm α}
{g₂ : Equiv.Perm α}
{s : Set α}
(h : Set.LeftInvOn (⇑g₁) (⇑g₂) s)
:
Set.LeftInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' s)
theorem
Set.RightInvOn.extendDomain
{α : Type u_1}
{β : Type u_2}
{p : β → Prop}
[DecidablePred p]
{f : α ≃ Subtype p}
{g₁ : Equiv.Perm α}
{g₂ : Equiv.Perm α}
{t : Set α}
(h : Set.RightInvOn (⇑g₁) (⇑g₂) t)
:
Set.RightInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' t)
theorem
Set.InvOn.extendDomain
{α : Type u_1}
{β : Type u_2}
{p : β → Prop}
[DecidablePred p]
{f : α ≃ Subtype p}
{g₁ : Equiv.Perm α}
{g₂ : Equiv.Perm α}
{s : Set α}
{t : Set α}
(h : Set.InvOn (⇑g₁) (⇑g₂) s t)
:
theorem
Set.SurjOn.prodMap
{α₁ : Type u_6}
{α₂ : Type u_7}
{β₁ : Type u_8}
{β₂ : Type u_9}
{s₁ : Set α₁}
{s₂ : Set α₂}
{t₁ : Set β₁}
{t₂ : Set β₂}
{f₁ : α₁ → β₁}
{f₂ : α₂ → β₂}
(h₁ : Set.SurjOn f₁ s₁ t₁)
(h₂ : Set.SurjOn f₂ s₂ t₂)
:
Set.SurjOn (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
theorem
Set.MapsTo.prodMap
{α₁ : Type u_6}
{α₂ : Type u_7}
{β₁ : Type u_8}
{β₂ : Type u_9}
{s₁ : Set α₁}
{s₂ : Set α₂}
{t₁ : Set β₁}
{t₂ : Set β₂}
{f₁ : α₁ → β₁}
{f₂ : α₂ → β₂}
(h₁ : Set.MapsTo f₁ s₁ t₁)
(h₂ : Set.MapsTo f₂ s₂ t₂)
:
Set.MapsTo (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
theorem
Set.LeftInvOn.prodMap
{α₁ : Type u_6}
{α₂ : Type u_7}
{β₁ : Type u_8}
{β₂ : Type u_9}
{s₁ : Set α₁}
{s₂ : Set α₂}
{f₁ : α₁ → β₁}
{f₂ : α₂ → β₂}
{g₁ : β₁ → α₁}
{g₂ : β₂ → α₂}
(h₁ : Set.LeftInvOn g₁ f₁ s₁)
(h₂ : Set.LeftInvOn g₂ f₂ s₂)
:
Set.LeftInvOn (fun (x : β₁ × β₂) => (g₁ x.1, g₂ x.2)) (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂)
theorem
Set.RightInvOn.prodMap
{α₁ : Type u_6}
{α₂ : Type u_7}
{β₁ : Type u_8}
{β₂ : Type u_9}
{t₁ : Set β₁}
{t₂ : Set β₂}
{f₁ : α₁ → β₁}
{f₂ : α₂ → β₂}
{g₁ : β₁ → α₁}
{g₂ : β₂ → α₂}
(h₁ : Set.RightInvOn g₁ f₁ t₁)
(h₂ : Set.RightInvOn g₂ f₂ t₂)
:
Set.RightInvOn (fun (x : β₁ × β₂) => (g₁ x.1, g₂ x.2)) (fun (x : α₁ × α₂) => (f₁ x.1, f₂ x.2)) (t₁ ×ˢ t₂)
theorem
Equiv.bijOn'
{α : Type u_1}
{β : Type u_2}
(e : α ≃ β)
{s : Set α}
{t : Set β}
(h₁ : Set.MapsTo (⇑e) s t)
(h₂ : Set.MapsTo (⇑e.symm) t s)
:
Set.BijOn (⇑e) s t
Alias of the forward direction of Equiv.bijOn_symm.
Alias of the reverse direction of Equiv.bijOn_symm.
theorem
Equiv.bijOn_swap
{α : Type u_1}
{s : Set α}
[DecidableEq α]
{a : α}
{b : α}
(ha : a ∈ s)
(hb : b ∈ s)
:
Set.BijOn (⇑(Equiv.swap a b)) s s