subset_iff — Mathlib

English

For any x,y in PSet, the inclusion mk x ⊆ mk y holds if and only if x ⊆ y.

Русский

Для любых x,y ∈ PSet верно: mk x ⊆ mk y ⇔ x ⊆ y.

LaTeX

$$$\forall {x y : \mathrm{PSet}}, mk x \subseteq mk y \iff x \subseteq y$$$

Lean4

@[simp]
theorem subset_iff : ∀ {x y : PSet}, mk x ⊆ mk y ↔ x ⊆ y
  | ⟨_, A⟩, ⟨_, _⟩ =>
    ⟨fun h a => @h ⟦A a⟧ (Mem.mk A a), fun h z =>
      Quotient.inductionOn z fun _ ⟨a, za⟩ =>
        let ⟨b, ab⟩ := h a
        ⟨b, za.trans ab⟩⟩

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