inter — Mathlib

English

If s and t are closed under f, then their intersection s ∩ t is closed under f.

Русский

Если s и t замкнуты относительно f, то их пересечение s ∩ t тоже замкнуто относительно f.

LaTeX

$$$$ (ClosedUnder\ f\ s) \land (ClosedUnder\ f\ t) \Rightarrow ClosedUnder\ f\ (s \cap t). $$$$

Lean4

theorem inter (hs : ClosedUnder f s) (ht : ClosedUnder f t) : ClosedUnder f (s ∩ t) := fun x h =>
  mem_inter (hs x fun i => mem_of_mem_inter_left (h i)) (ht x fun i => mem_of_mem_inter_right (h i))

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