image_val_union_self_left_eq — Mathlib

English

Let A be a subset of α and D a subset of A. Then the image of D under the inclusion into α, denoted ↑D, satisfies ↑D ∪ A = A.

Русский

Пусть A ⊆ α и D ⊆ A. Тогда образ D при включении в α, обозначаемый ↑D, удовлетворяет ↑D ∪ A = A.

LaTeX

$$$ D \subseteq A \Rightarrow (\uparrow D \cup A) = A $$$

Lean4

@[simp]
theorem image_val_union_self_left_eq : ↑D ∪ A = A :=
  union_eq_right.2 image_val_subset

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