Theorems · Theorem · order theory

Set.BijOn.exists_extend_of_subset

∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t : Set β} {f : α → β} {t' : Set β},
  Set.BijOn f s t → s ⊆ s₁ → t ⊆ t' → Set.SurjOn f s₁ t' → ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ Set.BijOn f s' t'

If f maps s bijectively to t and a set t' is contained in the image of some s₁ ⊇ s, then s₁ has a subset containing s that f maps bijectively to t'.

Defined in

Mathlib.Data.Set.Function

Cited by

2 results in Mathlib

Foundations

Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound