and — Mathlib

English

If two base-change properties P and Q hold, then their conjunction is stable under base-change.

Русский

Если два свойства P и Q сохраняются при базовом изменении, то их конъюнкция сохраняется.

LaTeX

$$$\text{IsStableUnderBaseChange}(P) \land \text{IsStableUnderBaseChange}(Q) \Rightarrow \text{IsStableUnderBaseChange}(\lambda f. P(f) \land Q(f)).$$$

Lean4

theorem and (hP : IsStableUnderBaseChange P) (hQ : IsStableUnderBaseChange Q) :
    IsStableUnderBaseChange (fun f ↦ P f ∧ Q f) := by
  introv R _ h
  exact ⟨hP R S R' S' h.1, hQ R S R' S' h.2⟩

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