image2_subset — Mathlib

English

image2 is monotone with respect to ⊆ in both arguments: if s ⊆ s' and t ⊆ t' then image2 f s t ⊆ image2 f s' t'.

Русский

image2 монотонна по отношению к ⊆ по обеим аргументам: если s ⊆ s' и t ⊆ t', то image2 f s t ⊆ image2 f s' t'.

LaTeX

$$If s ⊆ s' and t ⊆ t', then image2 f s t ⊆ image2 f s' t'.$$

Lean4

/-- image2 is monotone with respect to `⊆`. -/
@[gcongr]
theorem image2_subset (hs : s ⊆ s') (ht : t ⊆ t') : image2 f s t ⊆ image2 f s' t' :=
  by
  rintro _ ⟨a, ha, b, hb, rfl⟩
  exact mem_image2_of_mem (hs ha) (ht hb)

Похожие утверждения