mem_core — Mathlib

English

Let R be a relation between α and β and t ⊆ β. An element a ∈ α lies in the core of t with respect to R precisely when every element b related to a by R belongs to t.

Русский

Пусть R — отношение между α и β, и t ⊆ β. Элемент a ∈ α принадлежит ядру t относительно R тогда и только тогда, когда каждый элемент b, связанный с a отношением R, принадлежит t.

LaTeX

$$$a \in R.core t \iff \forall \{b\}, a ~[R] b \rightarrow b \in t$$$

Lean4

@[simp]
theorem mem_core : a ∈ R.core t ↔ ∀ ⦃b⦄, a ~[R] b → b ∈ t :=
  .rfl

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