and — Mathlib

English

The conjunction of two localization-span-type properties is again of localization-span type.

Русский

Сочетание двух свойств типа localization-span снова имеет тип localization-span.

LaTeX

$$$\\text{OfLocalizationSpanTarget }P \\land \\text{OfLocalizationSpanTarget }Q \\Rightarrow \\text{OfLocalizationSpanTarget }(P\\land Q)$$$

Lean4

theorem and (hP : OfLocalizationSpanTarget P) (hQ : OfLocalizationSpanTarget Q) :
    OfLocalizationSpanTarget (fun f ↦ P f ∧ Q f) := by
  introv R hs hf
  exact ⟨hP f s hs fun r ↦ (hf r).1, hQ f s hs fun r ↦ (hf r).2⟩

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