Set membership

Mathematical statement

Given a set A and an object x, x∈A is a proposition stating that x is an element of A.

Representative formula (exact TeX)

x\in A

Assumptions

• A has been specified as a set.

Symbol scope

• x — candidate element
• A — set
• ∈ — membership relation

Intuition, definition, and misconceptions

A set can be understood as a mathematical whole made up of selected objects, without requiring a physical box or spatial container.

The expression x∈A states only a membership relation. It does not say that x equals A, and it does not say that x is a subset of A.

In the current Lean mapping, Set α is represented as α→Prop, so x∈A and A x are definitionally equivalent.

A common mistake is to confuse element membership x∈A with the subset relation B⊆A, or to treat programming-container membership as the semantics of every mathematical set theory.

Adopted derivation guide

The original MKO is retained. The guide has its own append-only revision and verification boundaries, not a new Lean proof.

Prerequisites

Verification boundary

Lean formalizes membership when Set α is represented as α→Prop. This result does not claim to cover every foundation of set theory, and it does not automatically turn a programming container into a mathematical set.

formalized_lean_set_semantics

• evidence-sha256-702de77019f352eb431eb67bd7b266491b7c36c922d952e44be2b11ba95bcb5d

Next obligation

Extend the subset, set equality, and basic set-operation objects while keeping membership, inclusion, and equality as distinct relations.

Same-source structured data

This page and the interactive view use the same object and existing language edition; this adds no proof or human review.