Functions over sets #
Main definitions #
Predicate #
set.eq_on f₁ f₂ s: functionsf₁andf₂are equal at every point ofs;set.maps_to f s t:fsends every point ofsto a point oft;set.inj_on f s: restriction offtosis injective;set.surj_on f s t: every point inshas a preimage ins;set.bij_on f s t:fis a bijection betweensandt;set.left_inv_on f' f s: for everyx ∈ swe havef' (f x) = x;set.right_inv_on f' f t: for everyy ∈ twe havef (f' y) = y;set.inv_on f' f s t:f'is a two-side inverse offonsandt, i.e. we haveset.left_inv_on f' f sandset.right_inv_on f' f t.
Functions #
set.restrict f s: restrict the domain offto the sets;set.cod_restrict f s h: givenh : ∀ x, f x ∈ s, restrict the codomain offto the sets;set.maps_to.restrict f s t h: givenh : maps_to f s t, restrict the domain offtosand the codomain tot.
Restrict #
theorem
set.restrict_extend_range
{α : Type u}
{β : Type v}
{γ : Type w}
(f : α → β)
(g : α → γ)
(g' : β → γ) :
(set.range f).restrict (function.extend f g g') = λ (x : ↥(set.range f)), g (Exists.some _)
@[simp]
theorem
set.restrict_extend_compl_range
{α : Type u}
{β : Type v}
{γ : Type w}
(f : α → β)
(g : α → γ)
(g' : β → γ) :
theorem
set.range_extend_subset
{α : Type u}
{β : Type v}
{γ : Type w}
(f : α → β)
(g : α → γ)
(g' : β → γ) :
theorem
set.range_extend
{α : Type u}
{β : Type v}
{γ : Type w}
{f : α → β}
(hf : function.injective f)
(g : α → γ)
(g' : β → γ) :
def
set.cod_restrict
{α : Type u}
{β : Type v}
(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.cod_restrict f s h = λ (x : α), ⟨f x, _⟩
@[simp]
theorem
set.coe_cod_restrict_apply
{α : Type u}
{β : Type v}
(f : α → β)
(s : set β)
(h : ∀ (x : α), f x ∈ s)
(x : α) :
↑(set.cod_restrict f s h x) = f x
@[simp]
theorem
set.restrict_comp_cod_restrict
{α : Type u}
{β : Type v}
{γ : Type w}
{f : α → β}
{g : β → γ}
{b : set β}
(h : ∀ (x : α), f x ∈ b) :
b.restrict g ∘ set.cod_restrict f b h = g ∘ f
@[simp]
theorem
set.injective_cod_restrict
{α : Type u}
{β : Type v}
{t : set β}
{f : α → β}
(h : ∀ (x : α), f x ∈ t) :
theorem
function.injective.cod_restrict
{α : Type u}
{β : Type v}
{t : set β}
{f : α → β}
(h : ∀ (x : α), f x ∈ t) :
function.injective f → function.injective (set.cod_restrict f t h)
Alias of injective_cod_restrict.
Equality on a set #
@[simp]
theorem
set.eq_on.symm
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β}
(h : set.eq_on f₁ f₂ s) :
set.eq_on f₂ f₁ s
Congruence lemmas #
theorem
monotone_on.congr
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β}
[preorder α]
[preorder β]
(h₁ : monotone_on f₁ s)
(h : set.eq_on f₁ f₂ s) :
monotone_on f₂ s
theorem
antitone_on.congr
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β}
[preorder α]
[preorder β]
(h₁ : antitone_on f₁ s)
(h : set.eq_on f₁ f₂ s) :
antitone_on f₂ s
theorem
strict_mono_on.congr
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β}
[preorder α]
[preorder β]
(h₁ : strict_mono_on f₁ s)
(h : set.eq_on f₁ f₂ s) :
strict_mono_on f₂ s
theorem
strict_anti_on.congr
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β}
[preorder α]
[preorder β]
(h₁ : strict_anti_on f₁ s)
(h : set.eq_on f₁ f₂ s) :
strict_anti_on f₂ s
theorem
set.eq_on.congr_monotone_on
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β}
[preorder α]
[preorder β]
(h : set.eq_on f₁ f₂ s) :
monotone_on f₁ s ↔ monotone_on f₂ s
theorem
set.eq_on.congr_antitone_on
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β}
[preorder α]
[preorder β]
(h : set.eq_on f₁ f₂ s) :
antitone_on f₁ s ↔ antitone_on f₂ s
theorem
set.eq_on.congr_strict_mono_on
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β}
[preorder α]
[preorder β]
(h : set.eq_on f₁ f₂ s) :
strict_mono_on f₁ s ↔ strict_mono_on f₂ s
theorem
set.eq_on.congr_strict_anti_on
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β}
[preorder α]
[preorder β]
(h : set.eq_on f₁ f₂ s) :
strict_anti_on f₁ s ↔ strict_anti_on f₂ s
maps to #
maps_to f a b means that the image of a is contained in b.
Equations
- set.maps_to f s t = ∀ ⦃x : α⦄, x ∈ s → f x ∈ t
def
set.maps_to.restrict
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α)
(t : set β)
(h : set.maps_to f s t) :
Given a map f sending s : set α into t : set β, restrict domain of f to s
and the codomain to t. Same as subtype.map.
Equations
- set.maps_to.restrict f s t h = subtype.map f h
@[simp]
theorem
set.maps_to.coe_restrict_apply
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h : set.maps_to f s t)
(x : ↥s) :
↑(set.maps_to.restrict f s t h x) = f ↑x
theorem
set.maps_to'
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
set.maps_to f s t ↔ f '' s ⊆ t
@[simp]
theorem
set.maps_to_singleton
{α : Type u}
{β : Type v}
{t : set β}
{f : α → β}
{x : α} :
set.maps_to f {x} t ↔ f x ∈ t
theorem
set.maps_to.image_subset
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h : set.maps_to f s t) :
theorem
set.maps_to.congr
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β}
(h₁ : set.maps_to f₁ s t)
(h : set.eq_on f₁ f₂ s) :
set.maps_to f₂ s t
theorem
set.eq_on.comp_right
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{f : α → β}
{g₁ g₂ : β → γ}
(hg : set.eq_on g₁ g₂ t)
(hf : set.maps_to f s t) :
theorem
set.eq_on.maps_to_iff
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β}
(H : set.eq_on f₁ f₂ s) :
set.maps_to f₁ s t ↔ set.maps_to f₂ s t
theorem
set.maps_to.comp
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{p : set γ}
{f : α → β}
{g : β → γ}
(h₁ : set.maps_to g t p)
(h₂ : set.maps_to f s t) :
set.maps_to (g ∘ f) s p
theorem
set.maps_to.iterate
{α : Type u}
{f : α → α}
{s : set α}
(h : set.maps_to f s s)
(n : ℕ) :
set.maps_to f^[n] s s
theorem
set.maps_to.iterate_restrict
{α : Type u}
{f : α → α}
{s : set α}
(h : set.maps_to f s s)
(n : ℕ) :
set.maps_to.restrict f s s h^[n] = set.maps_to.restrict f^[n] s s _
theorem
set.maps_to.mono
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β}
(hf : set.maps_to f s₁ t₁)
(hs : s₂ ⊆ s₁)
(ht : t₁ ⊆ t₂) :
set.maps_to f s₂ t₂
theorem
set.maps_to.mono_left
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t : set β}
{f : α → β}
(hf : set.maps_to f s₁ t)
(hs : s₂ ⊆ s₁) :
set.maps_to f s₂ t
theorem
set.maps_to.mono_right
{α : Type u}
{β : Type v}
{s : set α}
{t₁ t₂ : set β}
{f : α → β}
(hf : set.maps_to f s t₁)
(ht : t₁ ⊆ t₂) :
set.maps_to f s t₂
theorem
set.maps_to.union_union
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β}
(h₁ : set.maps_to f s₁ t₁)
(h₂ : set.maps_to f s₂ t₂) :
set.maps_to f (s₁ ∪ s₂) (t₁ ∪ t₂)
theorem
set.maps_to.union
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t : set β}
{f : α → β}
(h₁ : set.maps_to f s₁ t)
(h₂ : set.maps_to f s₂ t) :
set.maps_to f (s₁ ∪ s₂) t
@[simp]
theorem
set.maps_to_union
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t : set β}
{f : α → β} :
set.maps_to f (s₁ ∪ s₂) t ↔ set.maps_to f s₁ t ∧ set.maps_to f s₂ t
theorem
set.maps_to.inter
{α : Type u}
{β : Type v}
{s : set α}
{t₁ t₂ : set β}
{f : α → β}
(h₁ : set.maps_to f s t₁)
(h₂ : set.maps_to f s t₂) :
set.maps_to f s (t₁ ∩ t₂)
theorem
set.maps_to.inter_inter
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β}
(h₁ : set.maps_to f s₁ t₁)
(h₂ : set.maps_to f s₂ t₂) :
set.maps_to f (s₁ ∩ s₂) (t₁ ∩ t₂)
@[simp]
theorem
set.maps_to_inter
{α : Type u}
{β : Type v}
{s : set α}
{t₁ t₂ : set β}
{f : α → β} :
set.maps_to f s (t₁ ∩ t₂) ↔ set.maps_to f s t₁ ∧ set.maps_to f s t₂
theorem
set.maps_to_univ
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α) :
set.maps_to f s set.univ
theorem
set.maps_to_image
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α) :
set.maps_to f s (f '' s)
theorem
set.maps_to_preimage
{α : Type u}
{β : Type v}
(f : α → β)
(t : set β) :
set.maps_to f (f ⁻¹' t) t
theorem
set.maps_to_range
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α) :
set.maps_to f s (set.range f)
@[simp]
theorem
set.maps_image_to
{α : Type u}
{β : Type v}
{γ : Type w}
(f : α → β)
(g : γ → α)
(s : set γ)
(t : set β) :
set.maps_to f (g '' s) t ↔ set.maps_to (f ∘ g) s t
@[simp]
theorem
set.maps_univ_to
{α : Type u}
{β : Type v}
(f : α → β)
(s : set β) :
set.maps_to f set.univ s ↔ ∀ (a : α), f a ∈ s
@[simp]
theorem
set.maps_range_to
{α : Type u}
{β : Type v}
{γ : Type w}
(f : α → β)
(g : γ → α)
(s : set β) :
set.maps_to f (set.range g) s ↔ set.maps_to (f ∘ g) set.univ s
theorem
set.surjective_maps_to_image_restrict
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α) :
function.surjective (set.maps_to.restrict f s (f '' s) _)
theorem
set.maps_to.mem_iff
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h : set.maps_to f s t)
(hc : set.maps_to f sᶜ tᶜ)
{x : α} :
Injectivity on a set #
f is injective on a if the restriction of f to a is injective.
theorem
set.subsingleton.inj_on
{α : Type u}
{β : Type v}
{s : set α}
(hs : s.subsingleton)
(f : α → β) :
set.inj_on f s
@[simp]
theorem
set.inj_on.eq_iff
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
{x y : α}
(h : set.inj_on f s)
(hx : x ∈ s)
(hy : y ∈ s) :
theorem
set.inj_on.congr
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β}
(h₁ : set.inj_on f₁ s)
(h : set.eq_on f₁ f₂ s) :
set.inj_on f₂ s
theorem
set.eq_on.inj_on_iff
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β}
(H : set.eq_on f₁ f₂ s) :
set.inj_on f₁ s ↔ set.inj_on f₂ s
theorem
set.inj_on.mono
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{f : α → β}
(h : s₁ ⊆ s₂)
(ht : set.inj_on f s₂) :
set.inj_on f s₁
theorem
set.inj_on_union
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{f : α → β}
(h : disjoint s₁ s₂) :
set.inj_on f (s₁ ∪ s₂) ↔ set.inj_on f s₁ ∧ set.inj_on f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
theorem
set.inj_on_insert
{α : Type u}
{β : Type v}
{f : α → β}
{s : set α}
{a : α}
(has : a ∉ s) :
set.inj_on f (insert a s) ↔ set.inj_on f s ∧ f a ∉ f '' s
theorem
set.inj_on_of_injective
{α : Type u}
{β : Type v}
{f : α → β}
(h : function.injective f)
(s : set α) :
set.inj_on f s
theorem
function.injective.inj_on
{α : Type u}
{β : Type v}
{f : α → β}
(h : function.injective f)
(s : set α) :
set.inj_on f s
Alias of inj_on_of_injective.
theorem
set.inj_on.comp
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{f : α → β}
{g : β → γ}
(hg : set.inj_on g t)
(hf : set.inj_on f s)
(h : set.maps_to f s t) :
set.inj_on (g ∘ f) s
theorem
set.inj_on_iff_injective
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β} :
set.inj_on f s ↔ function.injective (s.restrict f)
theorem
set.inj_on.injective
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β} :
set.inj_on f s → function.injective (s.restrict f)
Alias of inj_on_iff_injective.
theorem
set.inj_on_preimage
{α : Type u}
{β : Type v}
{f : α → β}
{B : set (set β)}
(hB : B ⊆ 𝒫set.range f) :
set.inj_on (set.preimage f) B
theorem
set.inj_on.mem_of_mem_image
{α : Type u}
{β : Type v}
{s s₁ : set α}
{f : α → β}
{x : α}
(hf : set.inj_on f s)
(hs : s₁ ⊆ s)
(h : x ∈ s)
(h₁ : f x ∈ f '' s₁) :
x ∈ s₁
theorem
set.inj_on.mem_image_iff
{α : Type u}
{β : Type v}
{s s₁ : set α}
{f : α → β}
{x : α}
(hf : set.inj_on f s)
(hs : s₁ ⊆ s)
(hx : x ∈ s) :
theorem
set.inj_on.preimage_image_inter
{α : Type u}
{β : Type v}
{s s₁ : set α}
{f : α → β}
(hf : set.inj_on f s)
(hs : s₁ ⊆ s) :
theorem
set.eq_on.cancel_left
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{f₁ f₂ : α → β}
{g : β → γ}
(h : set.eq_on (g ∘ f₁) (g ∘ f₂) s)
(hg : set.inj_on g t)
(hf₁ : set.maps_to f₁ s t)
(hf₂ : set.maps_to f₂ s t) :
set.eq_on f₁ f₂ s
theorem
set.inj_on.cancel_left
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{f₁ f₂ : α → β}
{g : β → γ}
(hg : set.inj_on g t)
(hf₁ : set.maps_to f₁ s t)
(hf₂ : set.maps_to f₂ s t) :
Surjectivity on a set #
f is surjective from a to b if b is contained in the image of a.
Equations
- set.surj_on f s t = (t ⊆ f '' s)
theorem
set.surj_on.subset_range
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h : set.surj_on f s t) :
theorem
set.surj_on_image
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α) :
set.surj_on f s (f '' s)
theorem
set.surj_on.comap_nonempty
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h : set.surj_on f s t)
(ht : t.nonempty) :
s.nonempty
theorem
set.surj_on.congr
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β}
(h : set.surj_on f₁ s t)
(H : set.eq_on f₁ f₂ s) :
set.surj_on f₂ s t
theorem
set.eq_on.surj_on_iff
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β}
(h : set.eq_on f₁ f₂ s) :
set.surj_on f₁ s t ↔ set.surj_on f₂ s t
theorem
set.surj_on.mono
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β}
(hs : s₁ ⊆ s₂)
(ht : t₁ ⊆ t₂)
(hf : set.surj_on f s₁ t₂) :
set.surj_on f s₂ t₁
theorem
set.surj_on.union
{α : Type u}
{β : Type v}
{s : set α}
{t₁ t₂ : set β}
{f : α → β}
(h₁ : set.surj_on f s t₁)
(h₂ : set.surj_on f s t₂) :
set.surj_on f s (t₁ ∪ t₂)
theorem
set.surj_on.union_union
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β}
(h₁ : set.surj_on f s₁ t₁)
(h₂ : set.surj_on f s₂ t₂) :
set.surj_on f (s₁ ∪ s₂) (t₁ ∪ t₂)
theorem
set.surj_on.inter_inter
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β}
(h₁ : set.surj_on f s₁ t₁)
(h₂ : set.surj_on f s₂ t₂)
(h : set.inj_on f (s₁ ∪ s₂)) :
set.surj_on f (s₁ ∩ s₂) (t₁ ∩ t₂)
theorem
set.surj_on.inter
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t : set β}
{f : α → β}
(h₁ : set.surj_on f s₁ t)
(h₂ : set.surj_on f s₂ t)
(h : set.inj_on f (s₁ ∪ s₂)) :
set.surj_on f (s₁ ∩ s₂) t
theorem
set.surj_on.comp
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{p : set γ}
{f : α → β}
{g : β → γ}
(hg : set.surj_on g t p)
(hf : set.surj_on f s t) :
set.surj_on (g ∘ f) s p
theorem
set.surj_on_iff_surjective
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β} :
set.surj_on f s set.univ ↔ function.surjective (s.restrict f)
theorem
set.surj_on.image_eq_of_maps_to
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h₁ : set.surj_on f s t)
(h₂ : set.maps_to f s t) :
theorem
set.image_eq_iff_surj_on_maps_to
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
f '' s = t ↔ set.surj_on f s t ∧ set.maps_to f s t
theorem
set.surj_on.maps_to_compl
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h : set.surj_on f s t)
(h' : function.injective f) :
set.maps_to f sᶜ tᶜ
theorem
set.maps_to.surj_on_compl
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h : set.maps_to f s t)
(h' : function.surjective f) :
set.surj_on f sᶜ tᶜ
theorem
set.eq_on.cancel_right
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{f : α → β}
{g₁ g₂ : β → γ}
(hf : set.eq_on (g₁ ∘ f) (g₂ ∘ f) s)
(hf' : set.surj_on f s t) :
set.eq_on g₁ g₂ t
theorem
set.surj_on.cancel_right
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{f : α → β}
{g₁ g₂ : β → γ}
(hf : set.surj_on f s t)
(hf' : set.maps_to f s t) :
Bijectivity #
f is bijective from s to t if f is injective on s and f '' s = t.
Equations
- set.bij_on f s t = (set.maps_to f s t ∧ set.inj_on f s ∧ set.surj_on f s t)
theorem
set.bij_on.maps_to
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h : set.bij_on f s t) :
set.maps_to f s t
theorem
set.bij_on.inj_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h : set.bij_on f s t) :
set.inj_on f s
theorem
set.bij_on.surj_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h : set.bij_on f s t) :
set.surj_on f s t
theorem
set.bij_on.mk
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h₁ : set.maps_to f s t)
(h₂ : set.inj_on f s)
(h₃ : set.surj_on f s t) :
set.bij_on f s t
theorem
set.bij_on.inter
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β}
(h₁ : set.bij_on f s₁ t₁)
(h₂ : set.bij_on f s₂ t₂)
(h : set.inj_on f (s₁ ∪ s₂)) :
set.bij_on f (s₁ ∩ s₂) (t₁ ∩ t₂)
theorem
set.bij_on.union
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β}
(h₁ : set.bij_on f s₁ t₁)
(h₂ : set.bij_on f s₂ t₂)
(h : set.inj_on f (s₁ ∪ s₂)) :
set.bij_on f (s₁ ∪ s₂) (t₁ ∪ t₂)
theorem
set.bij_on.subset_range
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h : set.bij_on f s t) :
theorem
set.inj_on.bij_on_image
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
(h : set.inj_on f s) :
set.bij_on f s (f '' s)
theorem
set.bij_on.congr
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β}
(h₁ : set.bij_on f₁ s t)
(h : set.eq_on f₁ f₂ s) :
set.bij_on f₂ s t
theorem
set.eq_on.bij_on_iff
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β}
(H : set.eq_on f₁ f₂ s) :
set.bij_on f₁ s t ↔ set.bij_on f₂ s t
theorem
set.bij_on.image_eq
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h : set.bij_on f s t) :
theorem
set.bij_on.comp
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{p : set γ}
{f : α → β}
{g : β → γ}
(hg : set.bij_on g t p)
(hf : set.bij_on f s t) :
set.bij_on (g ∘ f) s p
theorem
set.bij_on.bijective
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(h : set.bij_on f s t) :
function.bijective (set.cod_restrict (s.restrict f) t _)
theorem
set.bij_on.compl
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(hst : set.bij_on f s t)
(hf : function.bijective f) :
set.bij_on f sᶜ tᶜ
left inverse #
g is a left inverse to f on a means that g (f x) = x for all x ∈ a.
Equations
- set.left_inv_on f' f s = ∀ ⦃x : α⦄, x ∈ s → f' (f x) = x
theorem
set.left_inv_on.eq_on
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
{f' : β → α}
(h : set.left_inv_on f' f s) :
theorem
set.left_inv_on.eq
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
{f' : β → α}
(h : set.left_inv_on f' f s)
{x : α}
(hx : x ∈ s) :
f' (f x) = x
theorem
set.left_inv_on.congr_left
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
{f₁' f₂' : β → α}
(h₁ : set.left_inv_on f₁' f s)
{t : set β}
(h₁' : set.maps_to f s t)
(heq : set.eq_on f₁' f₂' t) :
set.left_inv_on f₂' f s
theorem
set.left_inv_on.congr_right
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β}
{f₁' : β → α}
(h₁ : set.left_inv_on f₁' f₁ s)
(heq : set.eq_on f₁ f₂ s) :
set.left_inv_on f₁' f₂ s
theorem
set.left_inv_on.inj_on
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
{f₁' : β → α}
(h : set.left_inv_on f₁' f s) :
set.inj_on f s
theorem
set.left_inv_on.surj_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f' : β → α}
(h : set.left_inv_on f' f s)
(hf : set.maps_to f s t) :
set.surj_on f' t s
theorem
set.left_inv_on.maps_to
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f' : β → α}
(h : set.left_inv_on f' f s)
(hf : set.surj_on f s t) :
set.maps_to f' t s
theorem
set.left_inv_on.comp
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{f : α → β}
{g : β → γ}
{f' : β → α}
{g' : γ → β}
(hf' : set.left_inv_on f' f s)
(hg' : set.left_inv_on g' g t)
(hf : set.maps_to f s t) :
set.left_inv_on (f' ∘ g') (g ∘ f) s
theorem
set.left_inv_on.mono
{α : Type u}
{β : Type v}
{s s₁ : set α}
{f : α → β}
{f' : β → α}
(hf : set.left_inv_on f' f s)
(ht : s₁ ⊆ s) :
set.left_inv_on f' f s₁
theorem
set.left_inv_on.image_inter'
{α : Type u}
{β : Type v}
{s s₁ : set α}
{f : α → β}
{f' : β → α}
(hf : set.left_inv_on f' f s) :
theorem
set.left_inv_on.image_image
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
{f' : β → α}
(hf : set.left_inv_on f' f s) :
theorem
set.left_inv_on.image_image'
{α : Type u}
{β : Type v}
{s s₁ : set α}
{f : α → β}
{f' : β → α}
(hf : set.left_inv_on f' f s)
(hs : s₁ ⊆ s) :
Right inverse #
g is a right inverse to f on b if f (g x) = x for all x ∈ b.
Equations
- set.right_inv_on f' f t = set.left_inv_on f f' t
theorem
set.right_inv_on.eq_on
{α : Type u}
{β : Type v}
{t : set β}
{f : α → β}
{f' : β → α}
(h : set.right_inv_on f' f t) :
theorem
set.right_inv_on.eq
{α : Type u}
{β : Type v}
{t : set β}
{f : α → β}
{f' : β → α}
(h : set.right_inv_on f' f t)
{y : β}
(hy : y ∈ t) :
f (f' y) = y
theorem
set.left_inv_on.right_inv_on_image
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
{f' : β → α}
(h : set.left_inv_on f' f s) :
set.right_inv_on f' f (f '' s)
theorem
set.right_inv_on.congr_left
{α : Type u}
{β : Type v}
{t : set β}
{f : α → β}
{f₁' f₂' : β → α}
(h₁ : set.right_inv_on f₁' f t)
(heq : set.eq_on f₁' f₂' t) :
set.right_inv_on f₂' f t
theorem
set.right_inv_on.congr_right
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β}
{f' : β → α}
(h₁ : set.right_inv_on f' f₁ t)
(hg : set.maps_to f' t s)
(heq : set.eq_on f₁ f₂ s) :
set.right_inv_on f' f₂ t
theorem
set.right_inv_on.surj_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f' : β → α}
(hf : set.right_inv_on f' f t)
(hf' : set.maps_to f' t s) :
set.surj_on f s t
theorem
set.right_inv_on.maps_to
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f' : β → α}
(h : set.right_inv_on f' f t)
(hf : set.surj_on f' t s) :
set.maps_to f s t
theorem
set.right_inv_on.comp
{α : Type u}
{β : Type v}
{γ : Type w}
{t : set β}
{p : set γ}
{f : α → β}
{g : β → γ}
{f' : β → α}
{g' : γ → β}
(hf : set.right_inv_on f' f t)
(hg : set.right_inv_on g' g p)
(g'pt : set.maps_to g' p t) :
set.right_inv_on (f' ∘ g') (g ∘ f) p
theorem
set.right_inv_on.mono
{α : Type u}
{β : Type v}
{t t₁ : set β}
{f : α → β}
{f' : β → α}
(hf : set.right_inv_on f' f t)
(ht : t₁ ⊆ t) :
set.right_inv_on f' f t₁
theorem
set.inj_on.right_inv_on_of_left_inv_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f' : β → α}
(hf : set.inj_on f s)
(hf' : set.left_inv_on f f' t)
(h₁ : set.maps_to f s t)
(h₂ : set.maps_to f' t s) :
set.right_inv_on f f' s
theorem
set.eq_on_of_left_inv_on_of_right_inv_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f₁' f₂' : β → α}
(h₁ : set.left_inv_on f₁' f s)
(h₂ : set.right_inv_on f₂' f t)
(h : set.maps_to f₂' t s) :
set.eq_on f₁' f₂' t
theorem
set.surj_on.left_inv_on_of_right_inv_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f' : β → α}
(hf : set.surj_on f s t)
(hf' : set.right_inv_on f f' s) :
set.left_inv_on f f' t
Two-side inverses #
g is an inverse to f viewed as a map from a to b
Equations
- set.inv_on g f s t = (set.left_inv_on g f s ∧ set.right_inv_on g f t)
theorem
set.inv_on.symm
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f' : β → α}
(h : set.inv_on f' f s t) :
set.inv_on f f' t s
theorem
set.inv_on.mono
{α : Type u}
{β : Type v}
{s s₁ : set α}
{t t₁ : set β}
{f : α → β}
{f' : β → α}
(h : set.inv_on f' f s t)
(hs : s₁ ⊆ s)
(ht : t₁ ⊆ t) :
set.inv_on f' f s₁ t₁
theorem
set.inv_on.bij_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f' : β → α}
(h : set.inv_on f' f s t)
(hf : set.maps_to f s t)
(hf' : set.maps_to f' t s) :
set.bij_on 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 maps_to arguments can be deduced from
surj_on statements using left_inv_on.maps_to and right_inv_on.maps_to.
inv_fun_on is a left/right inverse #
noncomputable
def
function.inv_fun_on
{α : Type u}
{β : Type v}
[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.injective.inv_of_mem_range.
Equations
- function.inv_fun_on f s b = dite (∃ (a : α), a ∈ s ∧ f a = b) (λ (h : ∃ (a : α), a ∈ s ∧ f a = b), classical.some h) (λ (h : ¬∃ (a : α), a ∈ s ∧ f a = b), classical.choice _inst_1)
theorem
function.inv_fun_on_pos
{α : Type u}
{β : Type v}
[nonempty α]
{s : set α}
{f : α → β}
{b : β}
(h : ∃ (a : α) (H : a ∈ s), f a = b) :
function.inv_fun_on f s b ∈ s ∧ f (function.inv_fun_on f s b) = b
theorem
function.inv_fun_on_mem
{α : Type u}
{β : Type v}
[nonempty α]
{s : set α}
{f : α → β}
{b : β}
(h : ∃ (a : α) (H : a ∈ s), f a = b) :
function.inv_fun_on f s b ∈ s
theorem
function.inv_fun_on_eq
{α : Type u}
{β : Type v}
[nonempty α]
{s : set α}
{f : α → β}
{b : β}
(h : ∃ (a : α) (H : a ∈ s), f a = b) :
f (function.inv_fun_on f s b) = b
theorem
function.inv_fun_on_neg
{α : Type u}
{β : Type v}
[nonempty α]
{s : set α}
{f : α → β}
{b : β}
(h : ¬∃ (a : α) (H : a ∈ s), f a = b) :
function.inv_fun_on f s b = classical.choice _inst_1
theorem
set.inj_on.left_inv_on_inv_fun_on
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
[nonempty α]
(h : set.inj_on f s) :
set.left_inv_on (function.inv_fun_on f s) f s
theorem
set.inj_on.inv_fun_on_image
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{f : α → β}
[nonempty α]
(h : set.inj_on f s₂)
(ht : s₁ ⊆ s₂) :
function.inv_fun_on f s₂ '' (f '' s₁) = s₁
theorem
set.surj_on.right_inv_on_inv_fun_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
[nonempty α]
(h : set.surj_on f s t) :
set.right_inv_on (function.inv_fun_on f s) f t
theorem
set.bij_on.inv_on_inv_fun_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
[nonempty α]
(h : set.bij_on f s t) :
set.inv_on (function.inv_fun_on f s) f s t
theorem
set.surj_on.inv_on_inv_fun_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
[nonempty α]
(h : set.surj_on f s t) :
set.inv_on (function.inv_fun_on f s) f (function.inv_fun_on f s '' t) t
theorem
set.surj_on.maps_to_inv_fun_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
[nonempty α]
(h : set.surj_on f s t) :
set.maps_to (function.inv_fun_on f s) t s
theorem
set.surj_on.bij_on_subset
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
[nonempty α]
(h : set.surj_on f s t) :
set.bij_on f (function.inv_fun_on f s '' t) t
theorem
set.surj_on_iff_exists_bij_on_subset
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
set.surj_on f s t ↔ ∃ (s' : set α) (H : s' ⊆ s), set.bij_on f s' t
theorem
set.preimage_inv_fun_of_mem
{α : Type u}
{β : Type v}
[n : nonempty α]
{f : α → β}
(hf : function.injective f)
{s : set α}
(h : classical.choice n ∈ s) :
theorem
set.preimage_inv_fun_of_not_mem
{α : Type u}
{β : Type v}
[n : nonempty α]
{f : α → β}
(hf : function.injective f)
{s : set α}
(h : classical.choice n ∉ s) :
function.inv_fun f ⁻¹' s = f '' s
Monotone #
@[protected]
theorem
monotone.cod_restrict
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(h : monotone f)
{s : set β}
(hs : ∀ (x : α), f x ∈ s) :
monotone (set.cod_restrict f s hs)
@[protected]
theorem
monotone.range_factorization
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(h : monotone f) :
Piecewise defined function #
@[protected, instance]
Equations
theorem
set.piecewise_insert
{α : Type u}
{δ : α → Sort y}
(s : set α)
(f g : Π (i : α), δ i)
[Π (j : α), decidable (j ∈ s)]
[decidable_eq α]
(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}
{β : Type v}
(x : α)
[Π (y : α), decidable (y ∈ {x})]
[decidable_eq α]
(f g : α → β) :
{x}.piecewise f g = function.update g x (f x)
theorem
set.maps_to.piecewise_ite
{α : Type u}
{β : Type v}
{s s₁ s₂ : set α}
{t t₁ t₂ : set β}
{f₁ f₂ : α → β}
[Π (i : α), decidable (i ∈ s)]
(h₁ : set.maps_to f₁ (s₁ ∩ s) (t₁ ∩ t))
(h₂ : set.maps_to f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)) :
set.maps_to (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)
theorem
set.apply_piecewise₂
{α : Type u}
{δ : α → Sort y}
(s : set α)
(f g : Π (i : α), δ i)
[Π (j : α), decidable (j ∈ s)]
{δ' : α → Sort u_1}
{δ'' : α → Sort u_2}
(f' g' : Π (i : α), δ' i)
(h : Π (i : α), δ i → δ' i → δ'' i)
{x : α} :
theorem
set.piecewise_op₂
{α : Type u}
{δ : α → Sort y}
(s : set α)
(f g : Π (i : α), δ i)
[Π (j : α), decidable (j ∈ s)]
{δ' : α → Sort u_1}
{δ'' : α → Sort u_2}
(f' g' : Π (i : α), δ' i)
(h : Π (i : α), δ i → δ' i → δ'' i) :
theorem
set.injective_piecewise_iff
{α : Type u}
{β : Type v}
(s : set α)
[Π (j : α), decidable (j ∈ s)]
{f g : α → β} :
function.injective (s.piecewise f g) ↔ set.inj_on f s ∧ set.inj_on g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∉ s → f x ≠ g y
theorem
strict_mono_on.inj_on
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
{s : set α}
(H : strict_mono_on f s) :
set.inj_on f s
theorem
strict_anti_on.inj_on
{α : Type u}
{β : Type v}
[linear_order α]
[preorder β]
{f : α → β}
{s : set α}
(H : strict_anti_on f s) :
set.inj_on f s
theorem
strict_mono_on.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder α]
[preorder β]
[preorder γ]
{g : β → γ}
{f : α → β}
{s : set α}
{t : set β}
(hg : strict_mono_on g t)
(hf : strict_mono_on f s)
(hs : set.maps_to f s t) :
strict_mono_on (g ∘ f) s
theorem
strict_mono_on.comp_strict_anti_on
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder α]
[preorder β]
[preorder γ]
{g : β → γ}
{f : α → β}
{s : set α}
{t : set β}
(hg : strict_mono_on g t)
(hf : strict_anti_on f s)
(hs : set.maps_to f s t) :
strict_anti_on (g ∘ f) s
theorem
strict_anti_on.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder α]
[preorder β]
[preorder γ]
{g : β → γ}
{f : α → β}
{s : set α}
{t : set β}
(hg : strict_anti_on g t)
(hf : strict_anti_on f s)
(hs : set.maps_to f s t) :
strict_mono_on (g ∘ f) s
theorem
strict_anti_on.comp_strict_mono_on
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder α]
[preorder β]
[preorder γ]
{g : β → γ}
{f : α → β}
{s : set α}
{t : set β}
(hg : strict_anti_on g t)
(hf : strict_mono_on f s)
(hs : set.maps_to f s t) :
strict_anti_on (g ∘ f) s
theorem
strict_mono.cod_restrict
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(hf : strict_mono f)
{s : set β}
(hs : ∀ (x : α), f x ∈ s) :
strict_mono (set.cod_restrict f s hs)
theorem
function.injective.comp_inj_on
{α : Type u}
{β : Type v}
{γ : Type w}
{f : α → β}
{g : β → γ}
{s : set α}
(hg : function.injective g)
(hf : set.inj_on f s) :
set.inj_on (g ∘ f) s
theorem
function.surjective.surj_on
{α : Type u}
{β : Type v}
{f : α → β}
(hf : function.surjective f)
(s : set β) :
set.surj_on f set.univ s
theorem
function.left_inverse.left_inv_on
{α : Type u}
{β : Type v}
{f : α → β}
{g : β → α}
(h : function.left_inverse f g)
(s : set β) :
set.left_inv_on f g s
theorem
function.right_inverse.right_inv_on
{α : Type u}
{β : Type v}
{f : α → β}
{g : β → α}
(h : function.right_inverse f g)
(s : set α) :
set.right_inv_on f g s
theorem
function.left_inverse.right_inv_on_range
{α : Type u}
{β : Type v}
{f : α → β}
{g : β → α}
(h : function.left_inverse f g) :
set.right_inv_on f g (set.range g)
theorem
function.semiconj.maps_to_image
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
{s t : set α}
(h : function.semiconj f fa fb)
(ha : set.maps_to fa s t) :
set.maps_to fb (f '' s) (f '' t)
theorem
function.semiconj.maps_to_range
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
(h : function.semiconj f fa fb) :
set.maps_to fb (set.range f) (set.range f)
theorem
function.semiconj.surj_on_image
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
{s t : set α}
(h : function.semiconj f fa fb)
(ha : set.surj_on fa s t) :
set.surj_on fb (f '' s) (f '' t)
theorem
function.semiconj.surj_on_range
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
(h : function.semiconj f fa fb)
(ha : function.surjective fa) :
set.surj_on fb (set.range f) (set.range f)
theorem
function.semiconj.inj_on_image
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
{s : set α}
(h : function.semiconj f fa fb)
(ha : set.inj_on fa s)
(hf : set.inj_on f (fa '' s)) :
set.inj_on fb (f '' s)
theorem
function.semiconj.inj_on_range
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
(h : function.semiconj f fa fb)
(ha : function.injective fa)
(hf : set.inj_on f (set.range fa)) :
set.inj_on fb (set.range f)
theorem
function.semiconj.bij_on_image
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
{s t : set α}
(h : function.semiconj f fa fb)
(ha : set.bij_on fa s t)
(hf : set.inj_on f t) :
set.bij_on fb (f '' s) (f '' t)
theorem
function.semiconj.bij_on_range
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
(h : function.semiconj f fa fb)
(ha : function.bijective fa)
(hf : function.injective f) :
set.bij_on fb (set.range f) (set.range f)
theorem
function.semiconj.maps_to_preimage
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
(h : function.semiconj f fa fb)
{s t : set β}
(hb : set.maps_to fb s t) :
set.maps_to fa (f ⁻¹' s) (f ⁻¹' t)
theorem
function.semiconj.inj_on_preimage
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
(h : function.semiconj f fa fb)
{s : set β}
(hb : set.inj_on fb s)
(hf : set.inj_on f (f ⁻¹' s)) :
set.inj_on fa (f ⁻¹' s)
theorem
function.update_comp_eq_of_not_mem_range'
{α : Sort u_1}
{β : Type u_2}
{γ : β → Sort u_3}
[decidable_eq β]
(g : Π (b : β), γ b)
{f : α → β}
{i : β}
(a : γ i)
(h : i ∉ set.range f) :
(λ (j : α), function.update g i a (f j)) = λ (j : α), g (f j)
theorem
function.update_comp_eq_of_not_mem_range
{α : Sort u_1}
{β : Type u_2}
{γ : Sort u_3}
[decidable_eq β]
(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'