mem_inf — Mathlib

English

Let R be a commutative semiring and A an R-algebra. For any two Subalgebras S and T of A, an element x ∈ A lies in the infimum S ⊓ T precisely when x lies in S and in T.

Русский

Пусть R — коммутативное полуребро, A — R-алгебра. Пусть S и T — подпалгебры A. Тогда элемент x ∈ A принадлежит наименьшему общему элементу S ⊓ T тогда и только тогда, когда x ∈ S и x ∈ T.

LaTeX

$$$x \in S \cap T \iff x \in S \land x \in T$$$

Lean4

@[simp]
theorem mem_inf {S T : Subalgebra R A} {x : A} : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T :=
  Iff.rfl

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