finite_of_isWF — Mathlib

English

If s and t are WF in a linear order, then mulAntidiagonal s t a is finite.

Русский

Если s и t являются WF в линейном порядке, то mulAntidiagonal s t a конечна.

LaTeX

$$If s.IsWF and t.IsWF, then (mulAntidiagonal s t a).Finite.$$

Lean4

@[to_additive Set.AddAntidiagonal.finite_of_isWF]
theorem finite_of_isWF {s t : Set α} (hs : s.IsWF) (ht : t.IsWF) (a) : (mulAntidiagonal s t a).Finite :=
  finite_of_isPWO hs.isPWO ht.isPWO a

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