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
- Set.restrict s f x = f ↑x
Instances For
theorem
Set.restrict_eq
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set α)
:
Set.restrict s f = f ∘ Subtype.val
@[simp]
theorem
Set.restrict_apply
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set α)
(x : ↑s)
:
Set.restrict s f x = f ↑x
theorem
Set.restrict_eq_iff
{α : Type u_1}
{π : α → Type u_5}
{f : (a : α) → π a}
{s : Set α}
{g : (a : ↑s) → π ↑a}
:
Set.restrict s f = g ↔ ∀ (a : α) (ha : a ∈ s), f a = g { val := a, property := ha }
theorem
Set.eq_restrict_iff
{α : Type u_1}
{π : α → Type u_5}
{s : Set α}
{f : (a : ↑s) → π ↑a}
{g : (a : α) → π a}
:
f = Set.restrict s g ↔ ∀ (a : α) (ha : a ∈ s), f { val := a, property := ha } = g a
@[simp]
theorem
Set.range_restrict
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set α)
:
Set.range (Set.restrict s f) = f '' s
@[simp]
theorem
Set.restrict_ite
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(g : α → β)
(s : Set α)
[(x : α) → Decidable (x ∈ s)]
:
(Set.restrict s fun (a : α) => if a ∈ s then f a else g a) = Set.restrict s f
@[simp]
theorem
Set.restrict_ite_compl
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(g : α → β)
(s : Set α)
[(x : α) → Decidable (x ∈ s)]
:
(Set.restrict sᶜ fun (a : α) => if a ∈ s then f a else g a) = Set.restrict sᶜ g
@[simp]
theorem
Set.restrict_piecewise
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(g : α → β)
(s : Set α)
[(x : α) → Decidable (x ∈ s)]
:
Set.restrict s (Set.piecewise s f g) = Set.restrict s f
@[simp]
theorem
Set.restrict_piecewise_compl
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(g : α → β)
(s : Set α)
[(x : α) → Decidable (x ∈ s)]
:
Set.restrict sᶜ (Set.piecewise s f g) = Set.restrict sᶜ g
theorem
Set.restrict_extend_range
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(g : α → γ)
(g' : β → γ)
:
Set.restrict (Set.range f) (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.restrict (Set.range f)ᶜ (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 = { val := f x, property := ⋯ }
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.restrict_comp_codRestrict
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{f : ι → α}
{g : α → β}
{b : Set α}
(h : ∀ (x : ι), f x ∈ b)
:
Set.restrict b g ∘ Set.codRestrict f b h = g ∘ f
@[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 #
@[simp]
theorem
Set.restrict_eq_restrict_iff
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f₁ : α → β}
{f₂ : α → β}
:
Set.restrict s f₁ = Set.restrict s f₂ ↔ Set.EqOn f₁ f₂ s
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 (Set.restrict s 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 (Set.restrict s 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 = Set.restrict s 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
theorem
Set.MapsTo.nonempty
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.MapsTo f s t)
(hs : Set.Nonempty s)
:
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 : Set.Nonempty s → Set.Nonempty t)
:
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.range_restrictPreimage
{α : Type u_1}
{β : Type u_2}
(t : Set β)
(f : α → β)
:
Set.range (Set.restrictPreimage t f) = Subtype.val ⁻¹' Set.range f
theorem
Set.restrictPreimage_injective
{α : Type u_1}
{β : Type u_2}
(t : Set β)
{f : α → β}
(hf : Function.Injective f)
:
theorem
Set.restrictPreimage_surjective
{α : Type u_1}
{β : Type u_2}
(t : Set β)
{f : α → β}
(hf : Function.Surjective f)
:
theorem
Set.restrictPreimage_bijective
{α : Type u_1}
{β : Type u_2}
(t : Set β)
{f : α → β}
(hf : Function.Bijective f)
:
theorem
Function.Injective.restrictPreimage
{α : Type u_1}
{β : Type u_2}
(t : Set β)
{f : α → β}
(hf : Function.Injective f)
:
Alias of Set.restrictPreimage_injective.
theorem
Function.Surjective.restrictPreimage
{α : Type u_1}
{β : Type u_2}
(t : Set β)
{f : α → β}
(hf : Function.Surjective f)
:
Alias of Set.restrictPreimage_surjective.
theorem
Function.Bijective.restrictPreimage
{α : Type u_1}
{β : Type u_2}
(t : Set β)
{f : α → β}
(hf : Function.Bijective f)
:
Alias of Set.restrictPreimage_bijective.
Injectivity on a set #
theorem
Set.Subsingleton.injOn
{α : Type u_1}
{β : Type u_2}
{s : Set α}
(hs : Set.Subsingleton s)
(f : α → β)
:
Set.InjOn f s
@[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 (Set.restrict s f)
theorem
Set.InjOn.injective
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
:
Set.InjOn f s → Function.Injective (Set.restrict s 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)
:
@[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_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 : Set.Nonempty t)
:
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 : Set.Nonempty t → Set.Nonempty s)
:
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 (Set.restrict s 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)
:
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 : Set.Nonempty s ↔ Set.Nonempty t)
:
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.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.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 #
theorem
Monotone.restrict
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{f : α → β}
(h : Monotone f)
(s : Set α)
:
Monotone (Set.restrict s f)
Piecewise defined function #
@[simp]
theorem
Set.piecewise_empty
{α : Type u_1}
{δ : α → Sort u_6}
(f : (i : α) → δ i)
(g : (i : α) → δ i)
[(i : α) → Decidable (i ∈ ∅)]
:
Set.piecewise ∅ f g = g
@[simp]
theorem
Set.piecewise_univ
{α : Type u_1}
{δ : α → Sort u_6}
(f : (i : α) → δ i)
(g : (i : α) → δ i)
[(i : α) → Decidable (i ∈ Set.univ)]
:
Set.piecewise Set.univ f g = f
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)]
:
Set.piecewise (insert j s) f g = Function.update (Set.piecewise s f g) j (f j)
@[simp]
theorem
Set.piecewise_eq_of_mem
{α : Type u_1}
{δ : α → Sort u_6}
(s : Set α)
(f : (i : α) → δ i)
(g : (i : α) → δ i)
[(j : α) → Decidable (j ∈ s)]
{i : α}
(hi : i ∈ s)
:
Set.piecewise s f g i = f i
@[simp]
theorem
Set.piecewise_eq_of_not_mem
{α : Type u_1}
{δ : α → Sort u_6}
(s : Set α)
(f : (i : α) → δ i)
(g : (i : α) → δ i)
[(j : α) → Decidable (j ∈ s)]
{i : α}
(hi : i ∉ s)
:
Set.piecewise s f g i = g i
theorem
Set.piecewise_singleton
{α : Type u_1}
{β : Type u_2}
(x : α)
[(y : α) → Decidable (y ∈ {x})]
[DecidableEq α]
(f : α → β)
(g : α → β)
:
Set.piecewise {x} f g = Function.update g x (f x)
theorem
Set.piecewise_eqOn
{α : Type u_1}
{β : Type u_2}
(s : Set α)
[(j : α) → Decidable (j ∈ s)]
(f : α → β)
(g : α → β)
:
Set.EqOn (Set.piecewise s f g) f s
theorem
Set.piecewise_eqOn_compl
{α : Type u_1}
{β : Type u_2}
(s : Set α)
[(j : α) → Decidable (j ∈ s)]
(f : α → β)
(g : α → β)
:
Set.EqOn (Set.piecewise s f g) g sᶜ
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)
:
Set.piecewise s f₁ f₂ ≤ Set.piecewise s g₁ g₂
@[simp]
theorem
Set.piecewise_insert_of_ne
{α : Type u_1}
{δ : α → Sort u_6}
(s : Set α)
(f : (i : α) → δ i)
(g : (i : α) → δ i)
[(j : α) → Decidable (j ∈ s)]
{i : α}
{j : α}
(h : i ≠ j)
[(i : α) → Decidable (i ∈ insert j s)]
:
Set.piecewise (insert j s) f g i = Set.piecewise s f g i
@[simp]
theorem
Set.piecewise_compl
{α : Type u_1}
{δ : α → Sort u_6}
(s : Set α)
(f : (i : α) → δ i)
(g : (i : α) → δ i)
[(j : α) → Decidable (j ∈ s)]
[(i : α) → Decidable (i ∈ sᶜ)]
:
Set.piecewise sᶜ f g = Set.piecewise s g f
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 (Set.piecewise s f₁ f₂) (Set.ite s s₁ s₂) (Set.ite t 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}
(h : (i : α) → δ i → δ' i)
{x : α}
:
h x (Set.piecewise s f g x) = Set.piecewise s (fun (x : α) => h x (f x)) (fun (x : α) => h x (g x)) x
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 (Set.piecewise s f g x) (Set.piecewise s f' g' x) = Set.piecewise s (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}
(h : (i : α) → δ i → δ' i)
:
(Set.piecewise s (fun (x : α) => h x (f x)) fun (x : α) => h x (g x)) = fun (x : α) => h x (Set.piecewise s f g 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)
:
(Set.piecewise s (fun (x : α) => h x (f x) (f' x)) fun (x : α) => h x (g x) (g' x)) = fun (x : α) =>
h x (Set.piecewise s f g x) (Set.piecewise s f' g' x)
@[simp]
theorem
Set.piecewise_same
{α : Type u_1}
{δ : α → Sort u_6}
(s : Set α)
(f : (i : α) → δ i)
[(j : α) → Decidable (j ∈ s)]
:
Set.piecewise s f f = f
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 (Set.restrict s f) ↔ StrictMonoOn f s
theorem
StrictMono.of_restrict
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{f : α → β}
{s : Set α}
:
StrictMono (Set.restrict s f) → StrictMonoOn f s
Alias of the forward direction of strictMono_restrict.
theorem
StrictMonoOn.restrict
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{f : α → β}
{s : Set α}
:
StrictMonoOn f s → StrictMono (Set.restrict s f)
Alias of the reverse 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 (⇑(Equiv.Perm.extendDomain g 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 (⇑(Equiv.Perm.extendDomain g f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)
theorem
Set.BijOn.extendDomain
{α : Type u_1}
{β : Type u_2}
{p : β → Prop}
[DecidablePred p]
{f : α ≃ Subtype p}
{g : Equiv.Perm α}
{s : Set α}
{t : Set α}
(h : Set.BijOn (⇑g) s 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 (⇑(Equiv.Perm.extendDomain g₁ f)) (⇑(Equiv.Perm.extendDomain g₂ 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 (⇑(Equiv.Perm.extendDomain g₁ f)) (⇑(Equiv.Perm.extendDomain g₂ 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)
:
Set.InvOn (⇑(Equiv.Perm.extendDomain g₁ f)) (⇑(Equiv.Perm.extendDomain g₂ f)) (Subtype.val ∘ ⇑f '' s)
(Subtype.val ∘ ⇑f '' 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