union — Mathlib

English

If f and g are definable over A, then f ∪ g is definable over A.

Русский

Если f и g определимы над A, то f ∪ g определимо над A.

LaTeX

$$$A.Definable L f \rightarrow A.Definable L g \rightarrow A.Definable L (f \cup g).$$$

Lean4

@[simp]
theorem union {f g : Set (α → M)} (hf : A.Definable L f) (hg : A.Definable L g) : A.Definable L (f ∪ g) :=
  by
  rcases hf with ⟨φ, hφ⟩
  rcases hg with ⟨θ, hθ⟩
  refine ⟨φ ⊔ θ, ?_⟩
  ext
  rw [hφ, hθ, mem_setOf_eq, Formula.realize_sup, mem_union, mem_setOf_eq, mem_setOf_eq]

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