inf — Mathlib

English

If s and t are closed under f, then their intersection s ∩ t is closed under f, i.e., the infimum of two f-closed sets is f-closed.

Русский

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

LaTeX

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

Lean4

theorem inf (hs : ClosedUnder f s) (ht : ClosedUnder f t) : ClosedUnder f (s ⊓ t) :=
  hs.inter ht

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