mul_subset_range — Mathlib

English

If m is a map, and s,t are subsets with s,t ⊆ range m, then s * t ⊆ range m.

Русский

Если s и t подпали под образ m, то их произведение принадлежит образу m.

LaTeX

$$$ s * t \subseteq \mathrm{range}\ m $$$

Lean4

@[to_additive]
theorem mul_subset_range {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) : s * t ⊆ range m :=
  by
  rintro _ ⟨a, ha, b, hb, rfl⟩
  obtain ⟨a, rfl⟩ := hs ha
  obtain ⟨b, rfl⟩ := ht hb
  exact ⟨a * b, map_mul ..⟩

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