inter — 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 \cap g).$$$

Lean4

@[simp]
theorem inter {f g : Set (α → M)} (hf : A.Definable L f) (hg : A.Definable L g) : A.Definable L (f ∩ g) :=
  by
  rcases hf with ⟨φ, rfl⟩
  rcases hg with ⟨θ, rfl⟩
  refine ⟨φ ⊓ θ, ?_⟩
  ext
  simp

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