spelling of assumption set being the complement

Stream: mathlib4

[Christian Merten]

Which of these is the preferred spelling for assuming that two sets s and t are each others complement?

import Mathlib.Data.Set.Basic
variable {α : Type} {s t : Set α}

lemma opt1 (h : IsCompl s t) : True := trivial
lemma opt2 (h₁ : s ∪ t = Set.univ) (h₂ : s ∩ t = ∅) : True := trivial
lemma opt3 (h : s = tᶜ) : True := trivial

(All of these are in simp normal form).

[Yaël Dillies]

The first one

[Christian Merten]

Thanks

[Yaël Dillies]

But usually you would write s and s^compl. Is there a reason you are not doing that?

[Christian Merten]

Yes, the precise setup is I have two (injective) functions α → β and γ → β and I want to define a basis indexed by γ under the assumption that the images are complements in β.