coe_inf — Mathlib

English

For any two submonoids p and p' of M, the underlying set of their meet (intersection) is exactly the intersection of their underlying sets: (p ⊓ p') as a set equals p ∩ p'.

Русский

Для двух подмонойдов p и p' подмножество их пересечения (meet) как множество равно пересечению их множеств.

LaTeX

$$$((p \sqcap p' : \mathrm{Submonoid} M) : \mathrm{Set} M) = (p : \mathrm{Set} M) \cap p'$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_inf (p p' : Submonoid M) : ((p ⊓ p' : Submonoid M) : Set M) = (p : Set M) ∩ p' :=
  rfl

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