hom_eq_iff_le — Mathlib

English

For C in G.ComponentCompl L, h ⊆ L, D in G.ComponentCompl K, C.hom h = D if and only if the underlying sets satisfy C ⊆ D.

Русский

Для C в G.ComponentCompl L, h ⊆ L, D в G.ComponentCompl K, C.hom h = D тогда и только тогда, когда подмножество C ⊆ D выполняется на множествах.

LaTeX

$$$ C.hom(h) = D \\iff (C : Set V) \\subseteq (D : Set V) $$$

Lean4

theorem hom_eq_iff_le (C : G.ComponentCompl L) (h : K ⊆ L) (D : G.ComponentCompl K) :
    C.hom h = D ↔ (C : Set V) ⊆ (D : Set V) :=
  ⟨fun h' => h' ▸ C.subset_hom h, C.ind fun _ vnL vD => (vD ⟨vnL, rfl⟩).choose_spec⟩

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