hom_eq_iff_not_disjoint — Mathlib

English

For C in G.ComponentCompl L, h ⊆ L, D in G.ComponentCompl K, C.hom h = D iff not Disjoint (C) (D).

Русский

Для C в G.ComponentCompl L, h ⊆ L, D в G.ComponentCompl K, C.hom h = D эквивалентно тому, что C и D неDisjoint.

LaTeX

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

Lean4

theorem hom_eq_iff_not_disjoint (C : G.ComponentCompl L) (h : K ⊆ L) (D : G.ComponentCompl K) :
    C.hom h = D ↔ ¬Disjoint (C : Set V) (D : Set V) :=
  by
  rw [Set.not_disjoint_iff]
  constructor
  · rintro rfl
    refine C.ind fun x xnL => ?_
    exact ⟨x, ⟨xnL, rfl⟩, ⟨fun xK => xnL (h xK), rfl⟩⟩
  · refine C.ind fun x xnL => ?_
    rintro ⟨x, ⟨_, e₁⟩, _, rfl⟩
    rw [← e₁]
    rfl

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