Theorems · Theorem · order theory

Set.image2_subset_left

∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β},
  t ⊆ t' → Set.image2 f s t ⊆ Set.image2 f s t'

Defined in

Mathlib.Data.Set.NAry

Cited by

12 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms