inter — Mathlib

English

If s and t are IsRelLowerSet for P, then s ∩ t is IsRelLowerSet for P.

Русский

Если s и t — IsRelLowerSet для P, тогда s ∩ t — IsRelLowerSet для P.

LaTeX

$$$IsRelLowerSet\\;s\\;P \\land IsRelLowerSet\\;t\\;P \\rightarrow IsRelLowerSet\\; (s \\cap t) \\;P$$$

Lean4

theorem inter (hs : IsRelLowerSet s P) (ht : IsRelLowerSet t P) : IsRelLowerSet (s ∩ t) P := fun b ⟨bs, bt⟩ ↦
  by
  simp_all only [IsRelLowerSet, true_and]
  exact fun _ x y ↦ ⟨(hs bs).2 x y, (ht bt).2 x y⟩

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