and — Mathlib

English

General form: if two properties are stable under base-change, then the combined property is stable under base-change as well.

Русский

Обобщение: если два свойства устойчивы к базовому изменению, то их объединение также устойчиво к базовому изменению.

LaTeX

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

Lean4

theorem and (hP : StableUnderComposition P) (hQ : StableUnderComposition Q) :
    StableUnderComposition (fun f ↦ P f ∧ Q f) := by
  introv R hf hg
  exact ⟨hP f g hf.1 hg.1, hQ f g hf.2 hg.2⟩

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