closedUnder_univ — Mathlib

English

Let f be any n-ary operation on M. Then for every choice of inputs from the universe M, the output lies in M.

Русский

Пусть f — произвольная n-арная операция на M. Тогда для любых аргументов из M результат операции принадлежит M.

LaTeX

$$$$ \forall f : M^n \to M, \ \forall x_1,\dots, x_n \in M,\ f(x_1,\dots, x_n) \in M. $$$$

Lean4

@[simp]
theorem closedUnder_univ : ClosedUnder f (univ : Set M) := fun _ _ => mem_univ _

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