mem_filter_prod_trans — Mathlib

English

If s is transitive, and s ∈ f ×ˢ g and s ∈ g ×ˢ h, then s ∈ f ×ˢ h (under g.NeBot).

Русский

Если s транзитивно, и s ∈ f ×ˢ g, и s ∈ g ×ˢ h, тогда s ∈ f ×ˢ h при условии, что g не пусто.

LaTeX

$$$\text{Transitive}(s) \rightarrow s \in f \timesˢ g \rightarrow s \in g \timesˢ h \rightarrow s \in f \timesˢ h$$$

Lean4

theorem mem_filter_prod_trans {s : Set (X × X)} {f g h : Filter X} [g.NeBot] (hs : IsTransitiveRel s) (hfg : s ∈ f ×ˢ g)
    (hgh : s ∈ g ×ˢ h) : s ∈ f ×ˢ h :=
  Eventually.trans_prod (by simpa using hfg) (by simpa using hgh) hs

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