子集合

數學敘述

給定同一論域中的集合 A、B，A⊆B 當且僅當對每個對象 x，若 x∈A，則 x∈B。

代表公式（精確 TeX）

A\subseteq B

成立條件

• A 與 B 是同一 ambient type 或同一明示論域中的集合。

符號作用域

• A — 候選子集合
• B — 候選母集合
• ⊆ — 非嚴格子集合關係

直觀、定義與常見誤解

要證明 A⊆B，必須從任意 x∈A 出發，說明同一個 x 也屬於 B；只列出一個共同元素並不充分。

A⊆B 允許 A=B，所以它是非嚴格包含。若要表達 A 是 B 的嚴格子集合，還必須排除 A=B。

x∈A 與 A⊆B 的型別角色不同：前者比較元素與集合，後者比較兩個集合。在 Lean 的 Set α 中，兩個集合也必須共享元素型別 α。

常見誤解是把 x∈A 與 {x}⊆A 混為同一語句、認為 A⊆B 必須 A≠B，或只檢查部分元素便斷言包含。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 集合隸屬 — 子集合以每個元素的隸屬蘊含關係定義。

驗證界線

本條目是子集合定義的 AI 候選；有限列舉可重算具體包含關係，但不能證成任意集合上的普遍性質。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。

下一個義務

綁定 Set.Subset 的精確定義展開、Mathlib 版本與 axiom receipt，並保持非嚴格包含、嚴格包含及集合相等三者分離。

同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。