inter — Mathlib

English

IsRelUpperSet.inter: intersection of two IsRelUpperSet is IsRelUpperSet.

Русский

Пересечение двух IsRelUpperSet также является IsRelUpperSet.

LaTeX

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

Lean4

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

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