Theorems · Theorem · order theory

Set.injOn_union

∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f : α → β},
  Disjoint s₁ s₂ → (Set.InjOn f (s₁ ∪ s₂) ↔ Set.InjOn f s₁ ∧ Set.InjOn f s₂ ∧ ∀ x ∈ s₁, ∀ y ∈ s₂, f x ≠ f y)

Defined in

Mathlib.Data.Set.Function

Cited by

3 results in Mathlib

Foundations

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