def Set.image {α : Type u_1} {β : Type u_2} (f : α → β) (x : Set α) : Set β

Equations

• f '' x = (Relation.graph f).image x

def Set.preimage {α : Type u_1} {β : Type u_2} (f : α → β) (x : Set β) : Set α

Equations

• f ⁻¹' x = (Relation.graph f).preimage x

def Set.term_''_ : Lean.TrailingParserDescr

Equations

• Set.term_''_ = Lean.ParserDescr.trailingNode `Set.term_''_ 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " '' ") (Lean.ParserDescr.cat `term 81))

def Set.«term_⁻¹'_» : Lean.TrailingParserDescr

Equations

• Set.«term_⁻¹'_» = Lean.ParserDescr.trailingNode `Set.«term_⁻¹'_» 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⁻¹' ") (Lean.ParserDescr.cat `term 81))

@[simp]

theorem Set.mem_image_iff {α : Type u_1} {β : Type u_2} {x : Set α} {f : α → β} {b : β} : b ∈ f '' x ↔ ∃ (a : α), b = f a ∧ a ∈ x

@[simp]

theorem Set.mem_preimage_iff {α : Type u_1} {β : Type u_2} {y : Set β} {f : α → β} {a : α} : a ∈ f ⁻¹' y ↔ f a ∈ y

theorem Set.val_mem_image_of_mem {α : Type u_1} {β : Type u_2} {x : Set α} {f : α → β} {a : α} (h : a ∈ x) : f a ∈ f '' x

@[simp]

theorem Set.val_mem_image_univ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} : f a ∈ f '' Set.univ

theorem Function.image_mono {α : Type u_1} {β : Type u_2} {f : α → β} {x y : Set α} (h : x ⊆ y) : f '' x ⊆ f '' y

@[simp]

theorem Function.image_singleton {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} : f '' {a} = {f a}

@[simp]

theorem Function.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {g : γ → α} {h : δ → γ} : f ∘ g ∘ h = (f ∘ g) ∘ h

@[simp]

theorem Function.comp_id_left {α : Type u_1} {β : Type u_2} {f : α → β} : id ∘ f = f

@[simp]

theorem Function.comp_id_right {α : Type u_1} {β : Type u_2} {f : α → β} : f ∘ id = f

@[simp]

theorem Function.subset_preimage_image {α : Type u_1} {β : Type u_2} {f : α → β} {x : Set α} : x ⊆ f ⁻¹' (f '' x)

@[simp]

theorem Function.image_preimage_subset {α : Type u_1} {β : Type u_2} {f : α → β} {y : Set β} : f '' (f ⁻¹' y) ⊆ y

@[simp]

theorem Function.image_empty {α : Type u_1} {β : Type u_2} {f : α → β} : f '' ∅ = ∅

@[simp]

theorem Function.image_empty_iff_empty {α : Type u_1} {β : Type u_2} {f : α → β} {x : Set α} : f '' x = ∅ ↔ x = ∅

@[simp]

theorem Function.preimage_empty {α : Type u_1} {β : Type u_2} {f : α → β} : f ⁻¹' ∅ = ∅

@[simp]

theorem Function.preimage_univ {α : Type u_1} {β : Type u_2} {f : α → β} : f ⁻¹' Set.univ = Set.univ

theorem Function.preimage_mono {α : Type u_1} {β : Type u_2} {f : α → β} {y y' : Set β} (h : y ⊆ y') : f ⁻¹' y ⊆ f ⁻¹' y'

@[simp]

theorem Function.image_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} {z : Set γ} : f ∘ g '' z = f '' (g '' z)

@[simp]

theorem Function.preimage_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} {x : Set β} : f ∘ g ⁻¹' x = g ⁻¹' (f ⁻¹' x)

@[simp]

theorem Function.image_id {α : Type u_1} {x : Set α} : id '' x = x

@[simp]

theorem Function.preimage_id {α : Type u_1} {x : Set α} : id ⁻¹' x = x

def Function.IsConstant {α : Type u_1} {β : Type u_2} (f : α → β) : Prop

Equations

• Function.IsConstant f = ∀ (a a' : α), f a = f a'

@[simp]

theorem Function.Function.const_isConstant {α : Type u_1} {β : Type u_2} {a : α} : Function.IsConstant (Function.const β a)

def Function.fixpoints {α : Type u_1} (f : α → α) : Set α

Equations

• Function.fixpoints f = {a : α | f a = a}

@[simp]

theorem Function.mem_fixpoints {α : Type u_1} {f : α → α} {a : α} : a ∈ Function.fixpoints f ↔ f a = a

@[simp]

theorem Function.fixpoints_id {α : Type u_1} : Function.fixpoints id = Set.univ

theorem Function.fixpoints_subset_comp_self {α : Type u_1} {f : α → α} : Function.fixpoints f ⊆ Function.fixpoints (f ∘ f)

def Function.is_extension {α : Type u_1} {β : Type u_2} {x : Set α} (g : α → β) (f : ↥x → β) : Prop

Equations

• Function.is_extension g f = ∀ (a : ↥x), f a = g a.val

def Function.restriction {α : Type u_1} {β : Type u_2} (f : α → β) (x : Set α) : ↥x → β

Equations

• (f|_x) a = f a.val

def Function.«term_|__» : Lean.TrailingParserDescr

Equations

• Function.«term_|__» = Lean.ParserDescr.trailingNode `Function.«term_|__» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "|_") (Lean.ParserDescr.cat `term 91))

@[simp]

theorem Function.is_extension_of_restriction {α : Type u_1} {β : Type u_2} {f : α → β} {x : Set α} : Function.is_extension f (f|_x)

@[simp]

theorem Function.restriction_id {α : Type u_1} {x : Set α} : id|_x = fun (a : ↥x) => a.val

@[simp]

theorem Function.restriction_const {α : Type u_1} {β : Type u_2} {x : Set α} {b : β} : Function.const α b|_x = Function.const (↥x) b

theorem Function.restriction_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {z : Set γ} {g : γ → α} : (f ∘ g)|_z = f ∘ g|_z

def Function.Injective {α : Type u_1} {β : Type u_2} (f : α → β) : Prop

Equations

• Function.Injective f = ∀ (a a' : α), f a = f a' → a = a'

theorem Function.Injective.eq_iff {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Injective f) {a a' : α} : f a = f a' ↔ a = a'

theorem Function.inj_iff_neq_of_neq {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Injective f ↔ ∀ (a a' : α), a ≠ a' → f a ≠ f a'

theorem Function.Injective.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} (h : Function.Injective f) (h' : Function.Injective g) : Function.Injective (f ∘ g)

theorem Function.inj_of_comp_inj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} (h : Function.Injective (f ∘ g)) : Function.Injective g

theorem Function.inj_iff_preimage_eq {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Injective f ↔ ∀ (b : β) (a a' : α), a ∈ f ⁻¹' {b} → a' ∈ f ⁻¹' {b} → a = a'

theorem Function.restriction_inj_of_comp_inj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} (h : Function.Injective (f ∘ g)) : Function.Injective (f|_(g '' Set.univ))

@[simp]

theorem Function.inj_id {α : Type u_1} : Function.Injective id

@[simp]

theorem Function.comp_self_inj_iff_inj {α : Type u_1} {f : α → α} : Function.Injective (f ∘ f) ↔ Function.Injective f

theorem Function.Injective.restriction {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Injective f) {x : Set α} : Function.Injective (f|_x)

theorem Function.Injective.preimage_image {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Injective f) {x : Set α} : f ⁻¹' (f '' x) = x

def Function.Surjective {α : Type u_1} {β : Type u_2} (f : α → β) : Prop

Equations

• Function.Surjective f = (f '' Set.univ = Set.univ)

@[simp]

theorem Function.surj_iff {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Surjective f ↔ ∀ (b : β), ∃ (a : α), b = f a

theorem Function.Surjective.exists_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Surjective f) (b : β) : ∃ (a : α), b = f a

theorem Function.Surjective.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} (h : Function.Surjective f) (h' : Function.Surjective g) : Function.Surjective (f ∘ g)

theorem Function.surj_of_comp_surj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} (h : Function.Surjective (f ∘ g)) : Function.Surjective f

theorem Function.surj_iff_preimage_nonempty {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Surjective f ↔ ∀ (b : β), (f ⁻¹' {b}).Nonempty

theorem Function.surj_iff_empty_of_preimage_empty {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Surjective f ↔ ∀ (y : Set β), f ⁻¹' y = ∅ → y = ∅

@[simp]

theorem Function.surj_id {α : Type u_1} : Function.Surjective id

@[simp]

theorem Function.comp_self_surj_iff_surj {α : Type u_1} {f : α → α} : Function.Surjective (f ∘ f) ↔ Function.Surjective f

theorem Function.surjective_of_restriction {α : Type u_1} {β : Type u_2} {f : α → β} {x : Set α} (h : Function.Surjective (f|_x)) : Function.Surjective f

theorem Function.Surjective.image_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Surjective f) {y : Set β} : f '' (f ⁻¹' y) = y

def Function.corestrict {α : Type u_1} {β : Type u_2} (f : α → β) {y : Set β} (h : f '' Set.univ ⊆ y) : α → ↥y

Equations

• Function.corestrict f h a = ⟨f a, ⋯⟩

theorem Function.corestrict_surjective {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Surjective (Function.corestrict f ⋯)

@[simp]

theorem Function.coe_corestrict {α : Type u_1} {β : Type u_2} {f : α → β} {y : Set β} {h : f '' Set.univ ⊆ y} {a : α} : (Function.corestrict f h a).val = f a

@[simp]

theorem Function.corestrict_eq_iff {α : Type u_1} {β : Type u_2} {f g : α → β} {y : Set β} {h : f '' Set.univ ⊆ y} {h' : g '' Set.univ ⊆ y} : Function.corestrict f h = Function.corestrict g h' ↔ f = g

def Function.Bijective {α : Type u_1} {β : Type u_2} (f : α → β) : Prop

Equations

• Function.Bijective f = (Function.Injective f ∧ Function.Surjective f)

theorem Function.Bijective.inj {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Bijective f) : Function.Injective f

theorem Function.Bijective.surj {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Bijective f) : Function.Surjective f

theorem Function.bij_id {α : Type u_1} : Function.Bijective id

theorem Function.Bijective.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} (h : Function.Bijective f) (h' : Function.Bijective g) : Function.Bijective (f ∘ g)

theorem Function.bij_iff_inv_functional {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Bijective f ↔ (Relation.graph f).inv.Functional

noncomputable def Function.Bijective.inv {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Bijective f) (b : β) : α

Equations

• h.inv b = ⋯.choose

@[simp]

theorem Function.Bijective.inv_val_iff {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Bijective f) {a : α} {b : β} : h.inv b = a ↔ f a = b

@[simp]

theorem Function.Bijective.inv_val_val {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Bijective f) {a : α} : h.inv (f a) = a

@[simp]

theorem Function.Bijective.val_inv_val {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Bijective f) {b : β} : f (h.inv b) = b

@[simp]

theorem Function.comp_inv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} (h : Function.Bijective f) (h' : Function.Bijective g) : ⋯.inv = h'.inv ∘ h.inv

@[simp]

theorem Function.Bijective.inv_bij {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Bijective f) : Function.Bijective h.inv

@[simp]

theorem Function.Bijective.inv_inv {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Bijective f) : ⋯.inv = f

@[simp]

theorem Function.id_inv {α : Type u_1} (h : Function.Bijective id) : h.inv = id

theorem Function.Bijective.comp_inv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} (h : Function.Bijective f) (h' : Function.Bijective g) : ⋯.inv = h'.inv ∘ h.inv

def Function.IsRetractionOf {α : Type u_1} {β : Type u_2} (r : α → β) (g : β → α) : Prop

Equations

• Function.IsRetractionOf r g = (r ∘ g = id)

def Function.IsSectionOf {α : Type u_1} {β : Type u_2} (s : α → β) (g : β → α) : Prop

Equations

• Function.IsSectionOf s g = (g ∘ s = id)

def Function.HasRetraction {α : Type u_1} {β : Type u_2} (f : α → β) : Prop

Equations

• Function.HasRetraction f = ∃ (g : β → α), Function.IsRetractionOf g f

def Function.HasSection {α : Type u_1} {β : Type u_2} (f : α → β) : Prop

Equations

• Function.HasSection f = ∃ (g : β → α), Function.IsSectionOf g f

def Function.IsInverseOf {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) : Prop

Equations

• Function.IsInverseOf f g = (Function.IsRetractionOf f g ∧ Function.IsSectionOf f g)

def Function.HasInverse {α : Type u_1} {β : Type u_2} (f : α → β) : Prop

Equations

• Function.HasInverse f = ∃ (g : β → α), Function.IsInverseOf g f

theorem Function.IsInverseOf.fg_eq {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsInverseOf f g) {b : β} : f (g b) = b

theorem Function.IsInverseOf.gf_eq {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsInverseOf f g) {a : α} : g (f a) = a

theorem Function.IsRetractionOf.fg_eq {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsRetractionOf f g) {b : β} : f (g b) = b

theorem Function.IsSectionOf.gf_eq {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsSectionOf f g) {b : α} : g (f b) = b

theorem Function.Surjective.hasSection {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Surjective f) : Function.HasSection f

theorem Function.Injective.hasRetraction {α : Type u_1} {β : Type u_2} {f : α → β} [Nonempty α] (h : Function.Injective f) : Function.HasRetraction f

theorem Function.Surjective.comp_right_inj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} (h : Function.Surjective f) : Function.Injective fun (x : β → γ) => x ∘ f

theorem Function.Surjective.comp_left_surj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} (h : Function.Surjective f) : Function.Surjective fun (x : γ → α) => f ∘ x

theorem Function.Injective.comp_right_surj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} [Nonempty α] (h : Function.Injective f) : Function.Surjective fun (x : β → γ) => x ∘ f

theorem Function.Injective.comp_left_inj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} (h : Function.Injective f) : Function.Injective fun (x : γ → α) => f ∘ x

theorem Function.IsSectionOf.swap_retraction {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsSectionOf f g) : Function.IsRetractionOf g f

theorem Function.IsRetractionOf.swap_section {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsRetractionOf f g) : Function.IsSectionOf g f

theorem Function.IsSectionOf.inj {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsSectionOf f g) : Function.Injective f

theorem Function.IsSectionOf.surj {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsSectionOf f g) : Function.Surjective g

theorem Function.IsRetractionOf.inj {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsRetractionOf f g) : Function.Injective g

theorem Function.IsRetractionOf.surj {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsRetractionOf f g) : Function.Surjective f

theorem Function.IsInverseOf.symm {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsInverseOf f g) : Function.IsInverseOf g f

theorem Function.IsInverseOf.bij' {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsInverseOf f g) : Function.Bijective f

theorem Function.IsInverseOf.bij {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsInverseOf f g) : Function.Bijective g

theorem Function.IsSectionOf.section_eq_iff_image_eq {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {f' : α → β} (h : Function.IsSectionOf f g) (h' : Function.IsSectionOf f' g) (h'' : f '' Set.univ = f' '' Set.univ) : f = f'

theorem Function.IsInverseOf.eq_inv {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsInverseOf f g) : ⋯.inv = g

theorem Function.IsInverseOf.eq_inv' {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : Function.IsInverseOf f g) : ⋯.inv = f

theorem Function.IsInverseOf.isInverse_eq {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {f' : α → β} (h : Function.IsInverseOf f g) (h' : Function.IsInverseOf f' g) : f = f'

theorem Function.IsInverseOf.isInverse_eq' {α : Type u_1} {β : Type u_2} {f : α → β} {g g' : β → α} (h : Function.IsInverseOf f g) (h' : Function.IsInverseOf f g') : g = g'

theorem Function.IsRetractionOf.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → α} {f' : β → γ} {g' : γ → β} (h : Function.IsRetractionOf f g) (h' : Function.IsRetractionOf f' g') : Function.IsRetractionOf (f' ∘ f) (g ∘ g')

theorem Function.IsSectionOf.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → α} {f' : β → γ} {g' : γ → β} (h : Function.IsSectionOf f g) (h' : Function.IsSectionOf f' g') : Function.IsSectionOf (f' ∘ f) (g ∘ g')

theorem Function.IsInverseOf.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → α} {f' : β → γ} {g' : γ → β} (h : Function.IsInverseOf f g) (h' : Function.IsInverseOf f' g') : Function.IsInverseOf (f' ∘ f) (g ∘ g')

theorem Function.HasRetraction.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {f' : β → γ} (h : Function.HasRetraction f) (h' : Function.HasRetraction f') : Function.HasRetraction (f' ∘ f)

theorem Function.HasSection.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {f' : β → γ} (h : Function.HasSection f) (h' : Function.HasSection f') : Function.HasSection (f' ∘ f)

theorem Function.HasInverse.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {f' : β → γ} (h : Function.HasInverse f) (h' : Function.HasInverse f') : Function.HasInverse (f' ∘ f)

theorem Function.Bijective.inv_isInverseOf {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Bijective f) : Function.IsInverseOf h.inv f

theorem Function.hasInverse_iff_bij {α : Type u_1} {β : Type u_2} {f : α → β} : Function.HasInverse f ↔ Function.Bijective f

theorem Function.isRetraction_of_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {f' : β → γ} {g : γ → α} (h : Function.IsRetractionOf g (f' ∘ f)) : Function.IsRetractionOf (g ∘ f') f

theorem Function.isSection_of_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {f' : β → γ} {g : γ → α} (h : Function.IsSectionOf g (f' ∘ f)) : Function.IsSectionOf (f ∘ g) f'

theorem Function.surj_of_inj_comp_surj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {f' : β → γ} (h : Function.Surjective (f' ∘ f)) (h' : Function.Injective f') : Function.Surjective f

theorem Function.inj_of_surj_comp_inj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {f' : β → γ} (h : Function.Injective (f' ∘ f)) (h' : Function.Surjective f) : Function.Injective f'

theorem Function.isRetraction_of_comp_surj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {f' : β → γ} {g : γ → α} (h : Function.IsRetractionOf g (f' ∘ f)) (h' : Function.Surjective f) : Function.IsRetractionOf (f ∘ g) f'

theorem Function.isSection_of_comp_inj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {f' : β → γ} {g : γ → α} (h : Function.IsSectionOf g (f' ∘ f)) (h' : Function.Injective f') : Function.IsSectionOf (g ∘ f') f

theorem Function.bij_of_two_bij2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {f' : β → γ} {g : γ → α} (h : Function.Bijective (f ∘ g)) (h' : Function.Bijective (g ∘ f')) : Function.Bijective g

theorem Function.bij_of_two_bij1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {f' : β → γ} {g : γ → α} (h : Function.Bijective (f ∘ g)) (h' : Function.Bijective (g ∘ f')) : Function.Bijective f

theorem Function.bij_of_two_bij3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {f' : β → γ} {g : γ → α} (h : Function.Bijective (f ∘ g)) (h' : Function.Bijective (g ∘ f')) : Function.Bijective f'

theorem Function.bij_of_surj_surj_inj1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} {f' : β → γ} (h : Function.Surjective (f' ∘ f ∘ g)) (h' : Function.Surjective (f ∘ g ∘ f')) (h'' : Function.Injective (g ∘ f' ∘ f)) : Function.Bijective f'

theorem Function.bij_of_surj_inj2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} {f' : β → γ} (h' : Function.Surjective (f ∘ g ∘ f')) (h'' : Function.Injective (g ∘ f' ∘ f)) : Function.Bijective f

theorem Function.bij_of_surj_inj3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} {f' : β → γ} (h : Function.Surjective (f' ∘ f ∘ g)) (h'' : Function.Injective (g ∘ f' ∘ f)) : Function.Bijective g

theorem Function.Surjective.factor_after {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} (h : Function.Surjective f) (h' : ∀ (a a' : α), f a = f a' → g a = g a') : ∃! p : β → γ, g = p ∘ f

theorem Function.Injective.factor_before {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → β} (h : Function.Injective f) (h' : g '' Set.univ ⊆ f '' Set.univ) : ∃! i : γ → α, g = f ∘ i

@[simp]

theorem Function.into_unit_surjective {α : Type u_1} [Nonempty α] {f : α → Unit} : Function.Surjective f

@[simp]

theorem Function.out_of_unit_injective {α : Type u_1} {f : Unit → α} : Function.Injective f

theorem Function.curry_bijective {α : Type u_1} {β : Type u_2} {γ : Type u_3} : Function.Bijective Function.curry

theorem Function.uncurry_bijective {α : Type u_1} {β : Type u_2} {γ : Type u_3} : Function.Bijective Function.uncurry

theorem Function.curry_uncurry_inverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} : Function.IsInverseOf Function.curry Function.uncurry

def Function.Injection (α : Type u_5) (β : Type u_6) : Type (max 0 u_5 u_6)

Equations

• Function.Injection α β = { f : α → β // Function.Injective f }

def Function.Surjection (α : Type u_5) (β : Type u_6) : Type (max 0 u_5 u_6)

Equations

• Function.Surjection α β = { f : α → β // Function.Surjective f }

def Function.Bijection (α : Type u_5) (β : Type u_6) : Type (max 0 u_5 u_6)

Equations

• Function.Bijection α β = { f : α → β // Function.Bijective f }

instance Function.instCoeFunBijectionForall {α : Type u_5} {β : Type u_6} : CoeFun (Function.Bijection α β) fun (x : Function.Bijection α β) => α → β

Equations

• Function.instCoeFunBijectionForall = { coe := fun (f : Function.Bijection α β) => f.val }

instance Function.instCoeFunSurjectionForall {α : Type u_5} {β : Type u_6} : CoeFun (Function.Surjection α β) fun (x : Function.Surjection α β) => α → β

Equations

• Function.instCoeFunSurjectionForall = { coe := fun (f : Function.Surjection α β) => f.val }

instance Function.instCoeFunInjectionForall {α : Type u_5} {β : Type u_6} : CoeFun (Function.Injection α β) fun (x : Function.Injection α β) => α → β

Equations

• Function.instCoeFunInjectionForall = { coe := fun (f : Function.Injection α β) => f.val }

noncomputable def Function.Bijection.invfun {α : Type u_1} {β : Type u_2} (f : Function.Bijection α β) (b : β) : α

Equations

• f.invfun = ⋯.inv

noncomputable def Function.Bijection.inv {α : Type u_1} {β : Type u_2} (f : Function.Bijection α β) : Function.Bijection β α

Equations

• f.inv = ⟨⋯.inv, ⋯⟩

@[simp]

theorem Function.Bijection.val_inv_val {α : Type u_1} {β : Type u_2} (f : Function.Bijection α β) {b : β} : f.val (f.inv.val b) = b

@[simp]

theorem Function.Bijection.inv_val_val {α : Type u_1} {β : Type u_2} (f : Function.Bijection α β) {a : α} : f.inv.val (f.val a) = a

def Function.bijection_of_funcs {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) (h : ∀ (b : β), f (g b) = b) (h' : ∀ (a : α), g (f a) = a) : Function.Bijection α β

Equations

• Function.bijection_of_funcs f g h h' = ⟨f, ⋯⟩

def Function.bijection_univ {α : Type u_1} : Function.Bijection (↥Set.univ) α

Equations

• Function.bijection_univ = Function.bijection_of_funcs Subtype.val (fun (x : α) => ⟨x, True.intro⟩) ⋯ ⋯

theorem Subtype.coe.inj {α : Type u_1} {p : α → Prop} : Function.Injective fun (x : { x : α // p x }) => match x with | ⟨x, property⟩ => x

theorem Subtype.val_inj {α : Type u_1} {p : α → Prop} : Function.Injective Subtype.val

theorem Eq.rec_of_inj {ι' : Type u_5} {ι : Type u_6} {x : ι → Type u_7} {i i' : ι'} (f : ι' → ι) (h : f i = f i') (h' : Function.Injective f) (a : (i : ι') → x (f i)) : h ▸ a i = a i'

@[simp]

theorem Subtype.val_image {α : Type u_1} {t : Set α} : Subtype.val '' Set.univ = t

theorem Function.Bijective.preimage_eq {α : Type u_1} {β : Type u_2} {s : Set β} {f : α → β} (h : Function.Bijective f) : f ⁻¹' s = h.inv '' s

@[simp]

theorem Function.image_univ_restriction {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : f|_s '' Set.univ = f '' s

def bijection_of_eq {α : Type u_1} {s t : Set α} (h : s = t) : Function.Bijection ↥s ↥t

Equations

• bijection_of_eq h = ⟨fun (x : ↥s) => match x with | ⟨x, hx⟩ => ⟨x, ⋯⟩, ⋯⟩